Job 2745

CakeML:d8e4b557fdf4443759cec20fccf35ea64046035b
  Fix cmlPtreeConversionProps [Dec 09 23:13:34]
#1110 (efficient-cases-peg)
Merging into:a645a6729e99cd3f74da80badcd21a5de3fb88c8
  Merge pull request #1112 from CakeML/update-readme [Dec 10 16:15:14]
HOL:81404220103cb7dac8d837073e53e07f92dca26a
  Merge pull request #1358 from HOL-Theorem-Prover/sha2 [Dec 10 12:18:19]
Machine:lammmington

Dec 11 05:43:05 Claimed job
Dec 11 05:43:11 Building HOL
Dec 11 05:54:06 Starting developers
Dec 11 05:54:10 Finished developers                                               3s 128MB
Dec 11 05:54:11 Starting developers/bin
Dec 11 05:54:17 Finished developers/bin                                           5s 746MB
Dec 11 05:54:18 Starting compiler/proofs
Dec 11 07:36:18 Finished compiler/proofs                                    1h41m58s  46GB
Dec 11 07:36:19 Starting compiler/bootstrap/translation
Dec 11 13:32:25 Finished compiler/bootstrap/translation                     5h56m05s  99GB
Dec 11 13:32:26 Starting semantics/ffi
Dec 11 13:32:36 Finished semantics/ffi                                            9s 592MB
Dec 11 13:32:37 Starting semantics
Dec 11 13:32:39 Finished semantics                                                0s  53MB
Dec 11 13:32:39 Starting semantics/proofs
Dec 11 13:33:03 Finished semantics/proofs                                        22s 669MB
Dec 11 13:33:04 Starting semantics/alt_semantics
Dec 11 13:33:24 Finished semantics/alt_semantics                                 18s 605MB
Dec 11 13:33:24 Starting semantics/alt_semantics/proofs
Dec 11 13:43:48 Finished semantics/alt_semantics/proofs                       10m22s   2GB
Dec 11 13:43:49 Starting basis/pure
Dec 11 13:43:50 Finished basis/pure                                               0s  61MB
Dec 11 13:43:51 Starting translator
Dec 11 13:45:23 Finished translator                                            1m31s   3GB
Dec 11 13:45:24 Starting compiler/parsing
Dec 11 13:45:26 Finished compiler/parsing                                         0s  57MB
Dec 11 13:45:27 Starting characteristic
Dec 11 13:45:28 Finished characteristic                                           0s  84MB
Dec 11 13:45:29 Starting translator/monadic
Dec 11 13:45:31 Finished translator/monadic                                       0s  86MB
Dec 11 13:45:32 Starting basis
Dec 11 13:47:53 Finished basis                                                 2m20s   4GB
Dec 11 13:47:54 Starting compiler/inference
Dec 11 13:47:56 Finished compiler/inference                                       0s  85MB
Dec 11 13:47:57 Starting compiler/backend/reg_alloc
Dec 11 13:47:58 Finished compiler/backend/reg_alloc                               0s  53MB
Dec 11 13:47:59 Starting compiler/backend/gc
Dec 11 13:48:01 Finished compiler/backend/gc                                      1s 134MB
Dec 11 13:48:02 Starting compiler/backend
Dec 11 13:48:07 Finished compiler/backend                                         4s 270MB
Dec 11 13:48:08 Starting compiler/encoders/asm
Dec 11 13:48:10 Finished compiler/encoders/asm                                    0s  78MB
Dec 11 13:48:10 Starting compiler/encoders/x64
Dec 11 13:48:12 Finished compiler/encoders/x64                                    0s  86MB
Dec 11 13:48:13 Starting compiler/encoders/arm7
Dec 11 13:48:15 Finished compiler/encoders/arm7                                   0s  90MB
Dec 11 13:48:16 Starting compiler/encoders/arm8
Dec 11 13:48:17 Finished compiler/encoders/arm8                                   0s  88MB
Dec 11 13:48:18 Starting compiler/encoders/arm8_asl
Dec 11 15:51:04 Finished compiler/encoders/arm8_asl                         2h02m44s  39GB
Dec 11 15:51:05 Starting compiler/encoders/mips
Dec 11 15:51:07 Finished compiler/encoders/mips                                   0s  90MB
Dec 11 15:51:08 Starting compiler/encoders/riscv
Dec 11 15:51:10 Finished compiler/encoders/riscv                                  0s  90MB
Dec 11 15:51:11 Starting compiler/encoders/ag32
Dec 11 15:51:12 Finished compiler/encoders/ag32                                   0s  79MB
Dec 11 15:51:13 Starting compiler/backend/x64
Dec 11 15:51:15 Finished compiler/backend/x64                                     1s 122MB
Dec 11 15:51:16 Starting compiler/backend/arm7
Dec 11 15:51:18 Finished compiler/backend/arm7                                    1s 122MB
Dec 11 15:51:19 Starting compiler/backend/arm8
Dec 11 15:51:21 Finished compiler/backend/arm8                                    1s 122MB
Dec 11 15:51:22 Starting compiler/backend/mips
Dec 11 15:51:24 Finished compiler/backend/mips                                    1s 122MB
Dec 11 15:51:25 Starting compiler/backend/riscv
Dec 11 15:51:27 Finished compiler/backend/riscv                                   1s 122MB
Dec 11 15:51:28 Starting compiler/backend/ag32
Dec 11 15:52:36 Finished compiler/backend/ag32                                 1m06s   2GB
Dec 11 15:52:37 Starting compiler/parsing/proofs
Dec 11 15:52:38 Finished compiler/parsing/proofs                                  0s  65MB
Dec 11 15:52:39 Starting compiler/inference/proofs
Dec 11 15:52:41 Finished compiler/inference/proofs                                0s  86MB
Dec 11 15:52:42 Starting compiler/backend/semantics
Dec 11 15:55:54 Finished compiler/backend/semantics                            3m11s   2GB
Dec 11 15:55:55 Starting compiler/backend/reg_alloc/proofs
Dec 11 15:55:57 Finished compiler/backend/reg_alloc/proofs                        0s  88MB
Dec 11 15:55:58 Starting compiler/backend/proofs
Dec 11 15:56:47 Finished compiler/backend/proofs                                 48s   3GB
Dec 11 15:56:48 Starting compiler/backend/serialiser
Dec 11 15:56:50 Finished compiler/backend/serialiser                              1s 130MB
Dec 11 15:56:51 Starting compiler/encoders/x64/proofs
Dec 11 16:07:10 Finished compiler/encoders/x64/proofs                         10m17s   4GB
Dec 11 16:07:10 Starting compiler/encoders/arm7/proofs
Dec 11 16:20:35 Finished compiler/encoders/arm7/proofs                        13m23s  13GB
Dec 11 16:20:36 Starting compiler/encoders/arm8/proofs
Dec 11 16:27:25 Finished compiler/encoders/arm8/proofs                         6m48s   3GB
Dec 11 16:27:26 Starting compiler/encoders/arm8_asl/proofs
Dec 11 17:17:18 Finished compiler/encoders/arm8_asl/proofs                    49m50s  20GB
Dec 11 17:17:19 Starting compiler/encoders/mips/proofs
Dec 11 17:27:45 Finished compiler/encoders/mips/proofs                        10m24s   5GB
Dec 11 17:27:45 Starting compiler/encoders/riscv/proofs
Dec 11 17:35:59 Finished compiler/encoders/riscv/proofs                        8m13s   4GB
Dec 11 17:36:00 Starting compiler/encoders/ag32/proofs
Dec 11 17:38:53 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Dec 11 17:38:54 Starting compiler/backend/x64/proofs
Dec 11 17:39:24 Finished compiler/backend/x64/proofs                             29s   2GB
Dec 11 17:39:25 Starting compiler/backend/arm7/proofs
Dec 11 17:39:55 Finished compiler/backend/arm7/proofs                            28s   1GB
Dec 11 17:39:55 Starting compiler/backend/arm8/proofs
Dec 11 17:40:24 Finished compiler/backend/arm8/proofs                            27s   1GB
Dec 11 17:40:25 Starting compiler/backend/arm8_asl
Dec 11 17:40:45 Finished compiler/backend/arm8_asl                               19s   1GB
Dec 11 17:40:46 Starting compiler/backend/mips/proofs
Dec 11 17:41:18 Finished compiler/backend/mips/proofs                            30s   2GB
Dec 11 17:41:19 Starting compiler/backend/riscv/proofs
Dec 11 17:41:50 Finished compiler/backend/riscv/proofs                           30s   2GB
Dec 11 17:41:51 Starting compiler/backend/ag32/proofs
Dec 11 17:55:45 Finished compiler/backend/ag32/proofs                         13m53s   5GB
Dec 11 17:55:46 Starting compiler/backend/cv_compute
Dec 11 17:56:55 Finished compiler/backend/cv_compute                           1m07s   2GB
Dec 11 17:56:56 Starting cv_translator
Dec 11 18:14:23 Finished cv_translator                                        17m26s   7GB
Dec 11 18:14:24 Starting candle/set-theory
Dec 11 18:15:00 Finished candle/set-theory                                       35s   1GB
Dec 11 18:15:01 Starting candle/syntax-lib
Dec 11 18:15:02 Finished candle/syntax-lib                                        0s  59MB
Dec 11 18:15:03 Starting candle/standard/syntax
Dec 11 18:15:16 Finished candle/standard/syntax                                  11s 773MB
Dec 11 18:15:16 Starting candle/standard/semantics
Dec 11 18:17:16 Finished candle/standard/semantics                             1m58s   2GB
Dec 11 18:17:17 Starting candle/standard/monadic
Dec 11 18:17:19 Finished candle/standard/monadic                                  0s  92MB
Dec 11 18:17:19 Starting candle/standard/ml_kernel
Dec 11 18:19:05 Finished candle/standard/ml_kernel                             1m44s   4GB
Dec 11 18:19:06 Starting candle/overloading/syntax
Dec 11 18:22:16 Finished candle/overloading/syntax                             3m08s   2GB
Dec 11 18:22:17 Starting candle/overloading/semantics
Dec 11 18:33:30 Finished candle/overloading/semantics                         11m11s   5GB
Dec 11 18:33:30 Starting candle/overloading/monadic
Dec 11 18:35:47 Finished candle/overloading/monadic                            2m15s   2GB
Dec 11 18:35:48 Starting candle/overloading/ml_kernel
Dec 11 18:43:09 Finished candle/overloading/ml_kernel                          7m20s   6GB
Dec 11 18:43:10 Starting candle/overloading/ml_checker
Dec 11 18:45:22 Finished candle/overloading/ml_checker                         2m11s   6GB
Dec 11 18:45:23 Starting candle/prover
Dec 11 18:55:00 Finished candle/prover                                         9m36s   5GB
Dec 11 18:55:01 Starting pancake
Dec 11 18:55:23 Finished pancake                                                 21s 820MB
Dec 11 18:55:24 Starting pancake/ffi
Dec 11 18:55:25 Finished pancake/ffi                                              0s  11MB
Dec 11 18:55:26 Starting pancake/semantics
Dec 11 18:57:39 Finished pancake/semantics                                     2m11s   2GB
Dec 11 18:57:40 Starting pancake/parser
Dec 11 18:58:04 Finished pancake/parser                                          23s 429MB
Dec 11 18:58:05 Starting pancake/proofs
Dec 11 19:14:13 Finished pancake/proofs                                       16m07s   6GB
Dec 11 19:14:14 Starting compiler/dafny
Dec 11 19:16:41 Finished compiler/dafny                                        2m26s   8GB
Dec 11 19:16:42 Starting compiler/dafny/translation
Dec 11 19:33:49 Finished compiler/dafny/translation                           17m05s  19GB
Dec 11 19:33:50 Starting compiler/dafny/compilation
Dec 11 19:36:18 Finished compiler/dafny/compilation                            2m27s   7GB
Dec 11 19:36:19 Starting compiler/dafny/semantics
Dec 11 19:36:55 Finished compiler/dafny/semantics                                35s   1GB
Dec 11 19:36:56 Starting characteristic/examples
Dec 11 19:38:23 Finished characteristic/examples                               1m25s   5GB
Dec 11 19:38:24 Starting tutorial/solutions
Dec 11 19:40:47 Finished tutorial/solutions                                    2m21s   3GB
Dec 11 19:40:48 Starting translator/monadic/examples
Dec 11 19:43:40 Finished translator/monadic/examples                           2m51s   3GB
Dec 11 19:43:41 Starting examples
Dec 11 19:49:49 Finished examples                                              6m06s   4GB
Dec 11 19:49:50 Starting examples/compilation/x64
Dec 11 19:56:28 Finished examples/compilation/x64                              6m37s   4GB
Dec 11 19:56:28 Starting examples/compilation/x64/proofs
Dec 11 19:58:48 Finished examples/compilation/x64/proofs                       2m19s   3GB
Dec 11 19:58:49 Starting examples/compilation/ag32
Dec 11 20:00:34 Finished examples/compilation/ag32                             1m43s   3GB
Dec 11 20:00:35 Starting examples/compilation/ag32/proofs
Dec 11 20:01:34 Finished examples/compilation/ag32/proofs                        57s   4GB
Dec 11 20:01:34 Starting examples/lpr_checker
Dec 11 20:02:04 Finished examples/lpr_checker                                    28s   1GB
Dec 11 20:02:05 Starting examples/lpr_checker/array
Dec 11 20:28:22 Finished examples/lpr_checker/array                           26m16s  27GB
Dec 11 20:28:23 Starting examples/lpr_checker/array/compilation
Dec 11 20:30:10 Finished examples/lpr_checker/array/compilation                1m46s   7GB
Dec 11 20:30:11 Starting examples/lpr_checker/array/compilation/proofs
Dec 11 20:31:20 Finished examples/lpr_checker/array/compilation/proofs         1m07s   5GB
Dec 11 20:31:20 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 11 20:32:25 Finished examples/lpr_checker/array/compilation/proofsARM8     1m03s   6GB
Dec 11 20:32:26 Starting .
Dec 11 20:32:29 Finished .                                                        2s 275MB
Dec 11 20:32:30 Starting examples/xlrup_checker
Dec 11 20:33:04 Finished examples/xlrup_checker                                  33s   1GB
Dec 11 20:33:05 Starting examples/xlrup_checker/array
Dec 11 20:45:56 Finished examples/xlrup_checker/array                         12m49s   8GB
Dec 11 20:45:57 Starting examples/xlrup_checker/array/compilation
Dec 11 20:46:55 Finished examples/xlrup_checker/array/compilation                57s   4GB
Dec 11 20:46:56 Starting examples/xlrup_checker/array/compilation/proofs
Dec 11 20:47:53 Finished examples/xlrup_checker/array/compilation/proofs         56s   4GB
Dec 11 20:47:54 Starting examples/pseudo_bool
Dec 11 20:49:26 Finished examples/pseudo_bool                                  1m30s   2GB
Dec 11 20:49:27 Starting examples/pseudo_bool/cnf_encoding
Dec 11 20:49:56 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Dec 11 20:49:57 Starting examples/pseudo_bool/graph_encoding
Dec 11 20:50:41 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Dec 11 20:50:42 Starting examples/pseudo_bool/array
Dec 11 21:58:32 Finished examples/pseudo_bool/array                         1h07m48s  31GB
Dec 11 21:58:33 Starting examples/pseudo_bool/array/compilation
Dec 11 22:07:10 Finished examples/pseudo_bool/array/compilation                8m36s  17GB
Dec 11 22:07:11 Starting examples/pseudo_bool/array/compilation/proofs
Dec 11 22:09:38 Finished examples/pseudo_bool/array/compilation/proofs         2m26s   6GB
Dec 11 22:09:39 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 11 22:10:45 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m05s   6GB
Dec 11 22:10:46 Starting examples/opentheory
Dec 11 22:19:23 Finished examples/opentheory                                   8m36s   6GB
Dec 11 22:19:24 Starting examples/opentheory
Dec 11 22:19:26 Finished examples/opentheory                                      1s 122MB
Dec 11 22:19:27 Starting examples/opentheory/compilation
Dec 11 22:20:53 Finished examples/opentheory/compilation                       1m24s   5GB
Dec 11 22:20:54 Starting examples/opentheory/compilation/proofs
Dec 11 22:21:50 Finished examples/opentheory/compilation/proofs                  55s   4GB
Dec 11 22:21:51 Starting examples/opentheory/compilation/ag32
Dec 11 22:23:19 Finished examples/opentheory/compilation/ag32                  1m26s   6GB
Dec 11 22:23:19 Starting examples/opentheory/compilation/ag32/proofs
Dec 11 22:24:55 Finished examples/opentheory/compilation/ag32/proofs           1m34s   7GB
Dec 11 22:24:56 Starting examples/sat_encodings
Dec 11 22:25:57 Finished examples/sat_encodings                                  59s 901MB
Dec 11 22:25:57 Starting examples/sat_encodings/case_studies
Dec 11 22:27:42 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Dec 11 22:27:43 Starting examples/sat_encodings/translation
Dec 11 22:31:16 Finished examples/sat_encodings/translation                    3m32s   5GB
Dec 11 22:31:17 Starting examples/sat_encodings/translation/compilation
Dec 11 22:33:05 Finished examples/sat_encodings/translation/compilation        1m46s   4GB
Dec 11 22:33:06 Starting examples/deflate
Dec 11 22:33:34 Finished examples/deflate                                        27s 727MB
Dec 11 22:33:35 Starting examples/deflate/translation
Dec 11 22:34:32 Finished examples/deflate/translation                            56s   2GB
Dec 11 22:34:33 Starting examples/deflate/translation/compilation
Dec 11 22:35:22 Finished examples/deflate/translation/compilation                48s   3GB
Dec 11 22:35:23 Starting examples/vipr
Dec 11 22:38:49 Finished examples/vipr                                         3m24s   4GB
Dec 11 22:38:49 Starting examples/vipr/compilation
Dec 11 22:39:43 Finished examples/vipr/compilation                               52s   3GB
Dec 11 22:39:44 Starting translator/okasaki-examples
Dec 11 22:43:49 Finished translator/okasaki-examples                           4m03s   3GB
Dec 11 22:43:50 Starting translator/other-examples
Dec 11 22:46:54 Finished translator/other-examples                             3m03s   3GB
Dec 11 22:46:55 Starting compiler/parsing/tests
Dec 11 22:47:30 Finished compiler/parsing/tests                                  34s   1GB
Dec 11 22:47:30 Starting compiler/inference/tests
Dec 11 22:48:06 Finished compiler/inference/tests                                34s   2GB
Dec 11 22:48:07 Starting compiler/printing/test
Dec 11 22:49:16 Finished compiler/printing/test                                1m07s   4GB
Dec 11 22:49:17 Starting icing/flover
Dec 11 23:23:41 Finished icing/flover                                         34m23s   2GB
Dec 11 23:23:42 Starting icing/
Dec 11 23:51:01 Finished icing/                                               27m17s   4GB
Dec 11 23:51:02 Starting icing/examples
Dec 11 23:52:24 Finished icing/examples                                        1m21s   4GB
Dec 11 23:52:25 Starting compiler/repl
Dec 12 00:00:23 Finished compiler/repl                                         7m57s   7GB
Dec 12 00:00:24 Starting unverified/sexpr-bootstrap/x64/64
Dec 12 00:04:29 Finished unverified/sexpr-bootstrap/x64/64                     4m03s  18GB
Dec 12 00:04:30 Starting unverified/sexpr-bootstrap/x64/32
Dec 12 00:07:56 Finished unverified/sexpr-bootstrap/x64/32                     3m25s  16GB
Dec 12 00:07:57 Starting compiler/benchmarks
Dec 12 00:08:43 Finished compiler/benchmarks                                     45s 712MB
Dec 12 00:08:44 Starting compiler/bootstrap/compilation/x64/64
Dec 12 00:33:38 Finished compiler/bootstrap/compilation/x64/64                24m53s  80GB
Dec 12 00:33:39 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 12 00:57:13 Finished compiler/bootstrap/compilation/x64/64/proofs         23m32s  48GB
Dec 12 00:57:14 Starting compiler/bootstrap/compilation/x64/32
Dec 12 01:22:18 Finished compiler/bootstrap/compilation/x64/32                25m03s  71GB
Dec 12 01:22:19 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 12 01:26:42 Finished compiler/bootstrap/compilation/x64/32/proofs          4m22s  25GB
Dec 12 01:26:43 Starting compiler/bootstrap/compilation/arm8/64
Dec 12 02:01:56 Finished compiler/bootstrap/compilation/arm8/64               35m11s  85GB
Dec 12 02:01:57 Starting compiler/bootstrap/compilation/arm8/64/proofs
Dec 12 02:07:08 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m09s  29GB
Dec 12 02:07:09 Starting compiler/bootstrap/compilation/ag32/32
Dec 12 02:31:57 Finished compiler/bootstrap/compilation/ag32/32               24m47s  55GB
Dec 12 02:31:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 12 02:37:18 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m18s  30GB
Dec 12 02:37:19 SUCCESS