Job 2236

CakeML:02b4196c6f4e9a47347568a05dddd023d5487c7d
  update types.txt [Nov 13 07:38:41]
#974 (dominance)
Merging into:7101a3f2e0c3885412c05e63735ec6da155253ee
  Fix for adjusted Inductive syntax [Nov 08 21:36:03]
HOL:be29184419aaa27f96bbbf8fb1b90d0e40385c33
  [emacs-mode] Handle new Inductive label syntaxes [Nov 08 03:19:35]
Machine:pavlova

Nov 13 07:55:11 Claimed job
Nov 13 07:55:16 Reusing HOL
Nov 13 07:55:26 Starting developers
Nov 13 07:55:30 Finished developers                                               2s 229MB
Nov 13 07:55:31 Starting developers/bin
Nov 13 07:55:44 Finished developers/bin                                          12s   1GB
Nov 13 07:55:45 Starting compiler/proofs
Nov 13 09:37:42 Finished compiler/proofs                                    1h41m56s  33GB
Nov 13 09:37:43 Starting compiler/bootstrap/translation
Nov 13 17:52:09 Finished compiler/bootstrap/translation                     8h14m25s  77GB
Nov 13 17:52:10 Starting semantics/ffi
Nov 13 17:52:18 Finished semantics/ffi                                            7s 610MB
Nov 13 17:52:19 Starting semantics
Nov 13 17:52:20 Finished semantics                                                0s  66MB
Nov 13 17:52:21 Starting semantics/proofs
Nov 13 17:52:56 Finished semantics/proofs                                        34s   2GB
Nov 13 17:52:57 Starting semantics/alt_semantics
Nov 13 17:53:37 Finished semantics/alt_semantics                                 39s   1GB
Nov 13 17:53:38 Starting semantics/alt_semantics/proofs
Nov 13 18:04:43 Finished semantics/alt_semantics/proofs                       11m03s   6GB
Nov 13 18:04:44 Starting basis/pure
Nov 13 18:04:45 Finished basis/pure                                               0s  66MB
Nov 13 18:04:46 Starting translator
Nov 13 18:06:37 Finished translator                                            1m49s   3GB
Nov 13 18:06:38 Starting compiler/parsing
Nov 13 18:06:39 Finished compiler/parsing                                         0s  70MB
Nov 13 18:06:40 Starting characteristic
Nov 13 18:06:41 Finished characteristic                                           0s  86MB
Nov 13 18:06:42 Starting translator/monadic
Nov 13 18:06:44 Finished translator/monadic                                       0s  91MB
Nov 13 18:06:45 Starting basis
Nov 13 18:10:21 Finished basis                                                 3m35s   5GB
Nov 13 18:10:22 Starting compiler/inference
Nov 13 18:10:23 Finished compiler/inference                                       0s  81MB
Nov 13 18:10:24 Starting compiler/backend/reg_alloc
Nov 13 18:10:25 Finished compiler/backend/reg_alloc                               0s  66MB
Nov 13 18:10:26 Starting compiler/backend/gc
Nov 13 18:10:28 Finished compiler/backend/gc                                      0s 137MB
Nov 13 18:10:29 Starting compiler/backend
Nov 13 18:10:46 Finished compiler/backend                                        16s   1GB
Nov 13 18:10:47 Starting compiler/encoders/asm
Nov 13 18:10:49 Finished compiler/encoders/asm                                    0s  91MB
Nov 13 18:10:49 Starting compiler/encoders/x64
Nov 13 18:10:51 Finished compiler/encoders/x64                                    0s  90MB
Nov 13 18:10:52 Starting compiler/encoders/arm7
Nov 13 18:10:53 Finished compiler/encoders/arm7                                   0s  94MB
Nov 13 18:10:54 Starting compiler/encoders/arm8
Nov 13 18:10:55 Finished compiler/encoders/arm8                                   0s  90MB
Nov 13 18:10:56 Starting compiler/encoders/arm8_asl
Nov 13 18:13:15 Finished compiler/encoders/arm8_asl                            2m17s   1GB
Nov 13 18:13:16 Starting compiler/encoders/mips
Nov 13 18:13:17 Finished compiler/encoders/mips                                   0s  87MB
Nov 13 18:13:18 Starting compiler/encoders/riscv
Nov 13 18:13:19 Finished compiler/encoders/riscv                                  0s  90MB
Nov 13 18:13:20 Starting compiler/encoders/ag32
Nov 13 18:13:21 Finished compiler/encoders/ag32                                   0s  90MB
Nov 13 18:13:22 Starting compiler/backend/x64
Nov 13 18:13:24 Finished compiler/backend/x64                                     0s 132MB
Nov 13 18:13:25 Starting compiler/backend/arm7
Nov 13 18:13:27 Finished compiler/backend/arm7                                    0s 130MB
Nov 13 18:13:27 Starting compiler/backend/arm8
Nov 13 18:13:29 Finished compiler/backend/arm8                                    0s 122MB
Nov 13 18:13:30 Starting compiler/backend/mips
Nov 13 18:13:32 Finished compiler/backend/mips                                    0s 121MB
Nov 13 18:13:33 Starting compiler/backend/riscv
Nov 13 18:13:34 Finished compiler/backend/riscv                                   0s 121MB
Nov 13 18:13:35 Starting compiler/backend/ag32
Nov 13 18:14:56 Finished compiler/backend/ag32                                 1m19s   4GB
Nov 13 18:14:56 Starting compiler/parsing/proofs
Nov 13 18:14:58 Finished compiler/parsing/proofs                                  0s  72MB
Nov 13 18:14:59 Starting compiler/inference/proofs
Nov 13 18:15:00 Finished compiler/inference/proofs                                0s  86MB
Nov 13 18:15:01 Starting compiler/backend/semantics
Nov 13 18:16:25 Finished compiler/backend/semantics                            1m23s   2GB
Nov 13 18:16:26 Starting compiler/backend/reg_alloc/proofs
Nov 13 18:16:28 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Nov 13 18:16:29 Starting compiler/backend/proofs
Nov 13 18:17:31 Finished compiler/backend/proofs                               1m01s   2GB
Nov 13 18:17:32 Starting compiler/backend/serialiser
Nov 13 18:17:34 Finished compiler/backend/serialiser                              1s 202MB
Nov 13 18:17:35 Starting compiler/encoders/x64/proofs
Nov 13 18:26:58 Finished compiler/encoders/x64/proofs                          9m22s   5GB
Nov 13 18:26:59 Starting compiler/encoders/arm7/proofs
Nov 13 18:39:57 Finished compiler/encoders/arm7/proofs                        12m57s   8GB
Nov 13 18:39:58 Starting compiler/encoders/arm8/proofs
Nov 13 18:46:19 Finished compiler/encoders/arm8/proofs                         6m19s   6GB
Nov 13 18:46:19 Starting compiler/encoders/arm8_asl/proofs
Nov 13 19:00:18 Finished compiler/encoders/arm8_asl/proofs                    13m58s   4GB
Nov 13 19:00:19 Starting compiler/encoders/mips/proofs
Nov 13 19:10:17 Finished compiler/encoders/mips/proofs                         9m56s   7GB
Nov 13 19:10:18 Starting compiler/encoders/riscv/proofs
Nov 13 19:18:34 Finished compiler/encoders/riscv/proofs                        8m15s   6GB
Nov 13 19:18:35 Starting compiler/encoders/ag32/proofs
Nov 13 19:20:56 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Nov 13 19:20:57 Starting compiler/backend/x64/proofs
Nov 13 19:21:36 Finished compiler/backend/x64/proofs                             37s   3GB
Nov 13 19:21:37 Starting compiler/backend/arm7/proofs
Nov 13 19:22:25 Finished compiler/backend/arm7/proofs                            47s   3GB
Nov 13 19:22:25 Starting compiler/backend/arm8/proofs
Nov 13 19:23:05 Finished compiler/backend/arm8/proofs                            38s   3GB
Nov 13 19:23:06 Starting compiler/backend/arm8_asl
Nov 13 19:23:35 Finished compiler/backend/arm8_asl                               28s   2GB
Nov 13 19:23:36 Starting compiler/backend/mips/proofs
Nov 13 19:24:19 Finished compiler/backend/mips/proofs                            42s   3GB
Nov 13 19:24:20 Starting compiler/backend/riscv/proofs
Nov 13 19:25:10 Finished compiler/backend/riscv/proofs                           49s   3GB
Nov 13 19:25:10 Starting compiler/backend/ag32/proofs
Nov 13 19:38:03 Finished compiler/backend/ag32/proofs                         12m51s   5GB
Nov 13 19:38:04 Starting candle/set-theory
Nov 13 19:38:49 Finished candle/set-theory                                       44s   1GB
Nov 13 19:38:50 Starting candle/syntax-lib
Nov 13 19:38:51 Finished candle/syntax-lib                                        0s  68MB
Nov 13 19:38:52 Starting candle/standard/syntax
Nov 13 19:39:08 Finished candle/standard/syntax                                  15s   1GB
Nov 13 19:39:09 Starting candle/standard/semantics
Nov 13 19:41:33 Finished candle/standard/semantics                             2m22s   2GB
Nov 13 19:41:34 Starting candle/standard/monadic
Nov 13 19:41:35 Finished candle/standard/monadic                                  0s 104MB
Nov 13 19:41:36 Starting candle/standard/ml_kernel
Nov 13 19:43:28 Finished candle/standard/ml_kernel                             1m51s   6GB
Nov 13 19:43:29 Starting candle/overloading/syntax
Nov 13 19:46:55 Finished candle/overloading/syntax                             3m24s   2GB
Nov 13 19:46:56 Starting candle/overloading/semantics
Nov 13 19:58:08 Finished candle/overloading/semantics                         11m12s   4GB
Nov 13 19:58:09 Starting candle/overloading/monadic
Nov 13 20:00:43 Finished candle/overloading/monadic                            2m32s   3GB
Nov 13 20:00:44 Starting candle/overloading/ml_kernel
Nov 13 20:08:16 Finished candle/overloading/ml_kernel                          7m31s   6GB
Nov 13 20:08:17 Starting candle/overloading/ml_checker
Nov 13 20:10:51 Finished candle/overloading/ml_checker                         2m32s   7GB
Nov 13 20:10:51 Starting candle/prover
Nov 13 20:20:38 Finished candle/prover                                         9m45s   5GB
Nov 13 20:20:39 Starting pancake
Nov 13 20:21:41 Finished pancake                                               1m00s   1GB
Nov 13 20:21:42 Starting pancake/ffi
Nov 13 20:21:42 Finished pancake/ffi                                              0s  21MB
Nov 13 20:21:43 Starting pancake/semantics
Nov 13 20:24:06 Finished pancake/semantics                                     2m21s   3GB
Nov 13 20:24:07 Starting pancake/parser
Nov 13 20:24:34 Finished pancake/parser                                          25s   1GB
Nov 13 20:24:35 Starting pancake/proofs
Nov 13 20:53:56 Finished pancake/proofs                                       29m20s   8GB
Nov 13 20:53:57 Starting characteristic/examples
Nov 13 20:55:34 Finished characteristic/examples                               1m36s   5GB
Nov 13 20:55:35 Starting tutorial/solutions
Nov 13 21:11:09 Finished tutorial/solutions                                   15m32s  13GB
Nov 13 21:11:10 Starting translator/monadic/examples
Nov 13 21:14:54 Finished translator/monadic/examples                           3m43s   5GB
Nov 13 21:14:55 Starting examples
Nov 13 21:29:37 Finished examples                                             14m40s   7GB
Nov 13 21:29:38 Starting examples/compilation/x64
Nov 13 23:25:59 Finished examples/compilation/x64                           1h56m20s  37GB
Nov 13 23:26:00 Starting examples/compilation/x64/proofs
Nov 13 23:29:47 Finished examples/compilation/x64/proofs                       3m45s   6GB
Nov 13 23:29:48 Starting examples/compilation/ag32
Nov 13 23:59:11 Finished examples/compilation/ag32                            29m22s  10GB
Nov 13 23:59:12 Starting examples/compilation/ag32/proofs
Nov 14 00:00:42 Finished examples/compilation/ag32/proofs                      1m29s   7GB
Nov 14 00:00:43 Starting examples/compilation/to_word
Nov 14 00:04:38 Finished examples/compilation/to_word                          3m54s  12GB
Nov 14 00:04:39 Starting examples/lpr_checker
Nov 14 00:05:54 Finished examples/lpr_checker                                  1m13s   2GB
Nov 14 00:05:55 Starting examples/lpr_checker/array
Nov 14 00:35:04 Finished examples/lpr_checker/array                           29m08s  19GB
Nov 14 00:35:05 Starting examples/lpr_checker/array/compilation
Nov 14 01:12:06 Finished examples/lpr_checker/array/compilation               37m00s  85GB
Nov 14 01:12:07 Starting examples/lpr_checker/array/compilation/proofs
Nov 14 01:14:01 Finished examples/lpr_checker/array/compilation/proofs         1m52s  10GB
Nov 14 01:14:02 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 14 01:37:16 Finished examples/lpr_checker/array/compilation/proofsARM8    23m12s  37GB
Nov 14 01:37:16 Starting examples/pseudo_bool
Nov 14 01:39:15 Finished examples/pseudo_bool                                  1m57s   2GB
Nov 14 01:39:16 Starting examples/pseudo_bool/cnf_encoding
Nov 14 01:39:51 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Nov 14 01:39:52 Starting examples/pseudo_bool/graph_encoding
Nov 14 01:40:41 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Nov 14 01:40:42 Starting examples/pseudo_bool/array
Nov 14 02:30:37 Finished examples/pseudo_bool/array                           49m53s  16GB
Nov 14 02:30:38 Starting examples/pseudo_bool/array/compilation
Nov 14 04:20:04 Finished examples/pseudo_bool/array/compilation             1h49m25s 115GB
Nov 14 04:20:05 Starting examples/pseudo_bool/array/compilation/proofs
Nov 14 04:23:10 Finished examples/pseudo_bool/array/compilation/proofs         3m04s   7GB
Nov 14 04:23:11 Starting examples/opentheory
Nov 14 04:33:42 Finished examples/opentheory                                  10m30s   7GB
Nov 14 04:33:43 Starting examples/opentheory
Nov 14 04:33:45 Finished examples/opentheory                                      0s 133MB
Nov 14 04:33:46 Starting examples/opentheory/compilation
Nov 14 05:09:25 Finished examples/opentheory/compilation                      35m37s  46GB
Nov 14 05:09:26 Starting examples/opentheory/compilation/proofs
Nov 14 05:10:55 Finished examples/opentheory/compilation/proofs                1m27s   6GB
Nov 14 05:10:55 Starting examples/opentheory/compilation/ag32
Nov 14 05:42:21 Finished examples/opentheory/compilation/ag32                 31m25s  44GB
Nov 14 05:42:22 Starting examples/opentheory/compilation/ag32/proofs
Nov 14 05:44:43 Finished examples/opentheory/compilation/ag32/proofs           2m19s  11GB
Nov 14 05:44:44 Starting examples/sat_encodings
Nov 14 05:47:23 Finished examples/sat_encodings                                2m38s   1GB
Nov 14 05:47:24 Starting examples/sat_encodings/case_studies
Nov 14 05:49:22 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Nov 14 05:49:23 Starting examples/sat_encodings/translation
Nov 14 05:55:23 Finished examples/sat_encodings/translation                    5m59s   7GB
Nov 14 05:55:24 Starting examples/sat_encodings/translation/compilation
Nov 14 06:30:15 Finished examples/sat_encodings/translation/compilation       34m50s  41GB
Nov 14 06:30:16 Starting examples/deflate
Nov 14 06:31:30 Finished examples/deflate                                      1m12s   1GB
Nov 14 06:31:31 Starting examples/deflate/translation
Nov 14 06:33:07 Finished examples/deflate/translation                          1m35s   7GB
Nov 14 06:33:08 Starting examples/deflate/translation/compilation
Nov 14 06:49:36 Finished examples/deflate/translation/compilation             16m26s  20GB
Nov 14 06:49:36 Starting examples/vipr
Nov 14 06:53:35 Finished examples/vipr                                         3m58s   5GB
Nov 14 06:53:36 Starting examples/vipr/compilation
Nov 14 07:12:58 Finished examples/vipr/compilation                            19m21s  32GB
Nov 14 07:12:59 Starting translator/okasaki-examples
Nov 14 07:17:54 Finished translator/okasaki-examples                           4m53s   4GB
Nov 14 07:17:55 Starting translator/other-examples
Nov 14 07:19:04 Finished translator/other-examples                             1m08s   3GB
Nov 14 07:19:04 Starting compiler/parsing/tests
Nov 14 07:19:38 Finished compiler/parsing/tests                                  32s   1GB
Nov 14 07:19:39 Starting compiler/inference/tests
Nov 14 07:27:07 Finished compiler/inference/tests                              7m27s   7GB
Nov 14 07:27:08 Starting compiler/printing/test
Nov 14 07:30:39 Finished compiler/printing/test                                3m29s   6GB
Nov 14 07:30:40 Starting icing/flover
Nov 14 08:06:43 Finished icing/flover                                         36m02s   4GB
Nov 14 08:06:44 Starting icing/
Nov 14 09:02:21 Finished icing/                                               55m36s  31GB
Nov 14 09:02:21 Starting icing/examples
Nov 14 09:04:03 Finished icing/examples                                        1m40s   8GB
Nov 14 09:04:03 Starting compiler/repl
Nov 14 09:12:43 Finished compiler/repl                                         8m38s  10GB
Nov 14 09:12:44 Starting unverified/sexpr-bootstrap/x64/64
Nov 14 09:23:36 Finished unverified/sexpr-bootstrap/x64/64                    10m50s  15GB
Nov 14 09:23:36 Starting unverified/sexpr-bootstrap/x64/32
Nov 14 09:32:38 Finished unverified/sexpr-bootstrap/x64/32                     9m00s  13GB
Nov 14 09:32:38 Starting compiler/benchmarks
Nov 14 09:33:23 Finished compiler/benchmarks                                     43s 713MB
Nov 14 09:33:24 Starting compiler/bootstrap/compilation/x64/64
Nov 14 23:39:46 Finished compiler/bootstrap/compilation/x64/64             14h06m21s 151GB
Nov 14 23:39:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 15 00:00:47 Finished compiler/bootstrap/compilation/x64/64/proofs         20m59s  46GB
Nov 15 00:00:48 Starting compiler/bootstrap/compilation/x64/32
Nov 15 07:14:35 Finished compiler/bootstrap/compilation/x64/32              7h13m45s 120GB
Nov 15 07:14:36 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 15 07:18:05 Finished compiler/bootstrap/compilation/x64/32/proofs          3m27s  18GB
Nov 15 07:18:05 Starting compiler/bootstrap/compilation/ag32/32
Nov 15 14:49:57 Finished compiler/bootstrap/compilation/ag32/32             7h31m50s 129GB
Nov 15 14:49:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 15 14:57:20 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m21s  40GB
Nov 15 14:57:20 SUCCESS