Job 2415

CakeML:2780707afbdb6e74a467fa3b48416f8101518335
  Replace occurrences of numLib.prefer_num with numLib.temp_prefer_num [Jun 17 02:03:55]
HOL:12a868b624d0e467c5adb2aa32d05577e2834525
  Remove some uses of >> for THEN1 [Jun 16 05:44:15]
Machine:lammmington
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Jun 17 02:14:20 Claimed job
Jun 17 02:14:28 Reusing HOL
Jun 17 02:14:39 Starting developers
Jun 17 02:14:43 Finished developers                                               2s 221MB
Jun 17 02:14:44 Starting developers/bin
Jun 17 02:15:03 Finished developers/bin                                          17s   1GB
Jun 17 02:15:04 Starting compiler/proofs
Jun 17 04:07:32 Finished compiler/proofs                                    1h52m27s  32GB
Jun 17 04:07:33 Starting compiler/bootstrap/translation
Jun 17 12:32:12 Finished compiler/bootstrap/translation                     8h24m38s  67GB
Jun 17 12:32:13 Starting semantics/ffi
Jun 17 12:32:22 Finished semantics/ffi                                            7s 649MB
Jun 17 12:32:23 Starting semantics
Jun 17 12:32:24 Finished semantics                                                0s  68MB
Jun 17 12:32:25 Starting semantics/proofs
Jun 17 12:33:02 Finished semantics/proofs                                        35s   1GB
Jun 17 12:33:03 Starting semantics/alt_semantics
Jun 17 12:33:45 Finished semantics/alt_semantics                                 41s   1GB
Jun 17 12:33:46 Starting semantics/alt_semantics/proofs
Jun 17 12:44:56 Finished semantics/alt_semantics/proofs                       11m08s   3GB
Jun 17 12:44:57 Starting basis/pure
Jun 17 12:44:58 Finished basis/pure                                               0s  71MB
Jun 17 12:44:59 Starting translator
Jun 17 12:46:50 Finished translator                                            1m49s   4GB
Jun 17 12:46:51 Starting compiler/parsing
Jun 17 12:46:52 Finished compiler/parsing                                         0s  76MB
Jun 17 12:46:53 Starting characteristic
Jun 17 12:46:55 Finished characteristic                                           0s  88MB
Jun 17 12:46:56 Starting translator/monadic
Jun 17 12:46:57 Finished translator/monadic                                       0s  96MB
Jun 17 12:46:58 Starting basis
Jun 17 12:50:30 Finished basis                                                 3m30s   5GB
Jun 17 12:50:31 Starting compiler/inference
Jun 17 12:50:33 Finished compiler/inference                                       1s 182MB
Jun 17 12:50:34 Starting compiler/backend/reg_alloc
Jun 17 12:50:35 Finished compiler/backend/reg_alloc                               0s  70MB
Jun 17 12:50:36 Starting compiler/backend/gc
Jun 17 12:50:38 Finished compiler/backend/gc                                      0s 138MB
Jun 17 12:50:39 Starting compiler/backend
Jun 17 12:50:59 Finished compiler/backend                                        19s   1GB
Jun 17 12:51:00 Starting compiler/encoders/asm
Jun 17 12:51:02 Finished compiler/encoders/asm                                    0s  90MB
Jun 17 12:51:03 Starting compiler/encoders/x64
Jun 17 12:51:04 Finished compiler/encoders/x64                                    0s 100MB
Jun 17 12:51:05 Starting compiler/encoders/arm7
Jun 17 12:51:07 Finished compiler/encoders/arm7                                   0s 101MB
Jun 17 12:51:08 Starting compiler/encoders/arm8
Jun 17 12:51:09 Finished compiler/encoders/arm8                                   0s 101MB
Jun 17 12:51:10 Starting compiler/encoders/arm8_asl
Jun 17 15:01:42 Finished compiler/encoders/arm8_asl                         2h10m31s  40GB
Jun 17 15:01:43 Starting compiler/encoders/mips
Jun 17 15:01:45 Finished compiler/encoders/mips                                   0s 103MB
Jun 17 15:01:46 Starting compiler/encoders/riscv
Jun 17 15:01:47 Finished compiler/encoders/riscv                                  0s  93MB
Jun 17 15:01:48 Starting compiler/encoders/ag32
Jun 17 15:01:50 Finished compiler/encoders/ag32                                   0s  99MB
Jun 17 15:01:51 Starting compiler/backend/x64
Jun 17 15:01:53 Finished compiler/backend/x64                                     0s 143MB
Jun 17 15:01:53 Starting compiler/backend/arm7
Jun 17 15:01:55 Finished compiler/backend/arm7                                    0s 142MB
Jun 17 15:01:56 Starting compiler/backend/arm8
Jun 17 15:01:58 Finished compiler/backend/arm8                                    0s 143MB
Jun 17 15:01:59 Starting compiler/backend/mips
Jun 17 15:02:01 Finished compiler/backend/mips                                    0s 142MB
Jun 17 15:02:02 Starting compiler/backend/riscv
Jun 17 15:02:04 Finished compiler/backend/riscv                                   0s 142MB
Jun 17 15:02:05 Starting compiler/backend/ag32
Jun 17 15:03:27 Finished compiler/backend/ag32                                 1m21s   2GB
Jun 17 15:03:28 Starting compiler/parsing/proofs
Jun 17 15:03:30 Finished compiler/parsing/proofs                                  0s  73MB
Jun 17 15:03:30 Starting compiler/inference/proofs
Jun 17 15:03:33 Finished compiler/inference/proofs                                1s 183MB
Jun 17 15:03:34 Starting compiler/backend/semantics
Jun 17 15:07:21 Finished compiler/backend/semantics                            3m46s   3GB
Jun 17 15:07:22 Starting compiler/backend/reg_alloc/proofs
Jun 17 15:07:24 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jun 17 15:07:25 Starting compiler/backend/proofs
Jun 17 15:08:29 Finished compiler/backend/proofs                               1m03s   3GB
Jun 17 15:08:29 Starting compiler/backend/serialiser
Jun 17 15:08:31 Finished compiler/backend/serialiser                              0s 138MB
Jun 17 15:08:32 Starting compiler/encoders/x64/proofs
Jun 17 15:17:56 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Jun 17 15:17:56 Starting compiler/encoders/arm7/proofs
Jun 17 15:30:39 Finished compiler/encoders/arm7/proofs                        12m41s   7GB
Jun 20 09:20:27 Resuming compiler/encoders/arm8/proofs
Jun 20 09:26:48 Finished compiler/encoders/arm8/proofs                         6m19s   4GB
Jun 20 09:26:49 Starting compiler/encoders/arm8_asl/proofs
Jun 20 10:14:14 Finished compiler/encoders/arm8_asl/proofs                    47m24s  12GB
Jun 20 10:14:15 Starting compiler/encoders/mips/proofs
Jun 20 10:24:24 Finished compiler/encoders/mips/proofs                        10m07s   8GB
Jun 20 10:24:25 Starting compiler/encoders/riscv/proofs
Jun 20 10:32:47 Finished compiler/encoders/riscv/proofs                        8m21s   4GB
Jun 20 10:32:48 Starting compiler/encoders/ag32/proofs
Jun 20 10:35:15 Finished compiler/encoders/ag32/proofs                         2m25s   4GB
Jun 20 10:35:16 Starting compiler/backend/x64/proofs
Jun 20 10:35:59 Finished compiler/backend/x64/proofs                             42s   3GB
Jun 20 10:36:00 Starting compiler/backend/arm7/proofs
Jun 20 10:36:45 Finished compiler/backend/arm7/proofs                            44s   2GB
Jun 20 10:36:46 Starting compiler/backend/arm8/proofs
Jun 20 10:37:27 Finished compiler/backend/arm8/proofs                            40s   2GB
Jun 20 10:37:28 Starting compiler/backend/arm8_asl
Jun 20 10:37:55 Finished compiler/backend/arm8_asl                               25s   1GB
Jun 20 10:37:56 Starting compiler/backend/mips/proofs
Jun 20 10:38:42 Finished compiler/backend/mips/proofs                            45s   3GB
Jun 20 10:38:43 Starting compiler/backend/riscv/proofs
Jun 20 10:39:34 Finished compiler/backend/riscv/proofs                           50s   4GB
Jun 20 10:39:35 Starting compiler/backend/ag32/proofs
Jun 20 10:55:28 Finished compiler/backend/ag32/proofs                         15m52s   6GB
Jun 20 10:55:29 Starting compiler/backend/cv_compute
Jun 20 10:57:16 Finished compiler/backend/cv_compute                           1m46s   3GB
Jun 20 10:57:17 Starting cv_translator
Jun 20 11:06:33 Finished cv_translator                                         9m15s   8GB
Jun 20 11:06:34 Starting candle/set-theory
Jun 20 11:07:23 Finished candle/set-theory                                       47s   1GB
Jun 20 11:07:24 Starting candle/syntax-lib
Jun 20 11:07:25 Finished candle/syntax-lib                                        0s  71MB
Jun 20 11:07:26 Starting candle/standard/syntax
Jun 20 11:07:44 Finished candle/standard/syntax                                  16s   1GB
Jun 20 11:07:45 Starting candle/standard/semantics
Jun 20 11:10:23 Finished candle/standard/semantics                             2m36s   3GB
Jun 20 11:10:24 Starting candle/standard/monadic
Jun 20 11:10:25 Finished candle/standard/monadic                                  0s 107MB
Jun 20 11:10:26 Starting candle/standard/ml_kernel
Jun 20 11:12:20 Finished candle/standard/ml_kernel                             1m52s   6GB
Jun 20 11:12:21 Starting candle/overloading/syntax
Jun 20 11:15:56 Finished candle/overloading/syntax                             3m34s   2GB
Jun 20 11:15:57 Starting candle/overloading/semantics
Jun 20 11:27:22 Finished candle/overloading/semantics                         11m24s   8GB
Jun 20 11:27:23 Starting candle/overloading/monadic
Jun 20 11:30:03 Finished candle/overloading/monadic                            2m38s   3GB
Jun 20 11:30:04 Starting candle/overloading/ml_kernel
Jun 20 11:37:46 Finished candle/overloading/ml_kernel                          7m41s   7GB
Jun 20 11:37:47 Starting candle/overloading/ml_checker
Jun 20 11:40:23 Finished candle/overloading/ml_checker                         2m34s   6GB
Jun 20 11:40:24 Starting candle/prover
Jun 20 11:50:26 Finished candle/prover                                        10m01s   5GB
Jun 20 11:50:27 Starting pancake
Jun 20 11:51:34 Finished pancake                                               1m06s   1GB
Jun 20 11:51:35 Starting pancake/ffi
Jun 20 11:51:36 Finished pancake/ffi                                              0s  23MB
Jun 20 11:51:37 Starting pancake/semantics
Jun 20 11:54:20 Finished pancake/semantics                                     2m42s   2GB
Jun 20 11:54:21 Starting pancake/parser
Jun 20 11:54:55 Finished pancake/parser                                          32s   2GB
Jun 20 11:54:56 Starting pancake/proofs
Jun 20 12:26:10 Finished pancake/proofs                                       31m13s   8GB
Jun 20 12:26:11 Starting characteristic/examples
Jun 20 12:27:50 Finished characteristic/examples                               1m37s   6GB
Jun 20 12:27:51 Starting tutorial/solutions
Jun 20 12:44:04 Finished tutorial/solutions                                   16m12s  20GB
Jun 20 12:44:05 Starting translator/monadic/examples
Jun 20 12:48:07 Finished translator/monadic/examples                           4m00s   5GB
Jun 20 12:48:07 Starting examples
Jun 20 13:02:41 Finished examples                                             14m32s   8GB
Jun 20 13:02:42 Starting examples/compilation/x64
Jun 20 15:04:18 Finished examples/compilation/x64                           2h01m35s  33GB
Jun 20 15:04:19 Starting examples/compilation/x64/proofs
Jun 20 15:08:19 Finished examples/compilation/x64/proofs                       3m58s   6GB
Jun 20 15:08:19 Starting examples/compilation/ag32
Jun 20 15:38:32 Finished examples/compilation/ag32                            30m11s  13GB
Jun 20 15:38:33 Starting examples/compilation/ag32/proofs
Jun 20 15:40:08 Finished examples/compilation/ag32/proofs                      1m33s   7GB
Jun 20 15:40:08 Starting examples/compilation/to_word
Jun 20 15:44:04 Finished examples/compilation/to_word                          3m55s  12GB
Jun 20 15:44:05 Starting examples/lpr_checker
Jun 20 15:45:29 Finished examples/lpr_checker                                  1m22s   2GB
Jun 20 15:45:30 Starting examples/lpr_checker/array
Jun 20 16:16:45 Finished examples/lpr_checker/array                           31m14s   9GB
Jun 20 16:16:46 Starting examples/lpr_checker/array/compilation
Jun 20 16:53:48 Finished examples/lpr_checker/array/compilation               37m00s  56GB
Jun 20 16:53:49 Starting examples/lpr_checker/array/compilation/proofs
Jun 20 16:55:35 Finished examples/lpr_checker/array/compilation/proofs         1m44s   8GB
Jun 20 16:55:36 Starting examples/lpr_checker/array/compilation/proofsARM8
Jun 20 17:04:22 Finished examples/lpr_checker/array/compilation/proofsARM8     8m45s  47GB
Jun 20 17:04:23 Starting examples/xlrup_checker
Jun 20 17:05:38 Finished examples/xlrup_checker                                1m14s   2GB
Jun 20 17:05:39 Starting examples/xlrup_checker/array
Jun 20 17:20:58 Finished examples/xlrup_checker/array                         15m18s   5GB
Jun 20 17:20:59 Starting examples/xlrup_checker/array/compilation
Jun 20 17:43:00 Finished examples/xlrup_checker/array/compilation             21m59s  44GB
Jun 20 17:43:00 Starting examples/xlrup_checker/array/compilation/proofs
Jun 20 17:44:41 Finished examples/xlrup_checker/array/compilation/proofs       1m39s   7GB
Jun 20 17:44:41 Starting examples/pseudo_bool
Jun 20 17:46:52 Finished examples/pseudo_bool                                  2m09s   2GB
Jun 20 17:46:53 Starting examples/pseudo_bool/cnf_encoding
Jun 20 17:47:33 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Jun 20 17:47:34 Starting examples/pseudo_bool/graph_encoding
Jun 20 17:48:26 Finished examples/pseudo_bool/graph_encoding                     51s   1GB
Jun 20 17:48:27 Starting examples/pseudo_bool/array
Jun 20 18:57:15 Finished examples/pseudo_bool/array                         1h08m47s  39GB
Jun 20 18:57:16 Starting examples/pseudo_bool/array/compilation
Jun 21 00:10:10 Finished examples/pseudo_bool/array/compilation             5h12m52s 154GB
Jun 21 00:10:11 Starting examples/pseudo_bool/array/compilation/proofs
Jun 21 00:13:50 Finished examples/pseudo_bool/array/compilation/proofs         3m37s   8GB
Jun 21 00:13:51 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jun 21 00:29:56 Finished examples/pseudo_bool/array/compilation/proofsARM8    16m03s  36GB
Jun 21 00:29:57 Starting examples/opentheory
Jun 21 00:40:42 Finished examples/opentheory                                  10m43s   8GB
Jun 21 00:40:43 Starting examples/opentheory
Jun 21 00:40:44 Finished examples/opentheory                                      0s 135MB
Jun 21 00:40:45 Starting examples/opentheory/compilation
Jun 21 01:17:13 Finished examples/opentheory/compilation                      36m27s  53GB
Jun 21 01:17:14 Starting examples/opentheory/compilation/proofs
Jun 21 01:18:45 Finished examples/opentheory/compilation/proofs                1m29s   6GB
Jun 21 01:18:45 Starting examples/opentheory/compilation/ag32
Jun 21 01:50:37 Finished examples/opentheory/compilation/ag32                 31m50s  39GB
Jun 21 01:50:38 Starting examples/opentheory/compilation/ag32/proofs
Jun 21 01:53:05 Finished examples/opentheory/compilation/ag32/proofs           2m25s  12GB
Jun 21 01:53:06 Starting examples/sat_encodings
Jun 21 01:56:04 Finished examples/sat_encodings                                2m57s   1GB
Jun 21 01:56:05 Starting examples/sat_encodings/case_studies
Jun 21 01:58:22 Finished examples/sat_encodings/case_studies                   2m16s   1GB
Jun 21 01:58:23 Starting examples/sat_encodings/translation
Jun 21 02:04:59 Finished examples/sat_encodings/translation                    6m35s   8GB
Jun 21 02:05:00 Starting examples/sat_encodings/translation/compilation
Jun 21 02:40:34 Finished examples/sat_encodings/translation/compilation       35m32s  50GB
Jun 21 02:40:35 Starting examples/deflate
Jun 21 02:42:00 Finished examples/deflate                                      1m24s   1GB
Jun 21 02:42:01 Starting examples/deflate/translation
Jun 21 02:43:43 Finished examples/deflate/translation                          1m41s   7GB
Jun 21 02:43:44 Starting examples/deflate/translation/compilation
Jun 21 03:00:37 Finished examples/deflate/translation/compilation             16m52s  19GB
Jun 21 03:00:38 Starting examples/vipr
Jun 21 03:04:47 Finished examples/vipr                                         4m07s   7GB
Jun 21 03:04:48 Starting examples/vipr/compilation
Jun 21 03:24:42 Finished examples/vipr/compilation                            19m53s  23GB
Jun 21 03:24:44 Starting translator/okasaki-examples
Jun 21 03:29:55 Finished translator/okasaki-examples                           5m10s   3GB
Jun 21 03:29:56 Starting translator/other-examples
Jun 21 03:34:42 Finished translator/other-examples                             4m43s   3GB
Jun 21 03:34:43 Starting compiler/parsing/tests
Jun 21 03:35:17 Finished compiler/parsing/tests                                  33s   1GB
Jun 21 03:35:18 Starting compiler/inference/tests
Jun 21 03:36:00 Finished compiler/inference/tests                                41s   2GB
Jun 21 03:36:01 Starting compiler/printing/test
Jun 21 03:37:35 Finished compiler/printing/test                                1m32s   7GB
Jun 21 03:37:36 Starting icing/flover
Jun 21 04:14:28 Finished icing/flover                                         36m51s   4GB
Jun 21 04:14:29 Starting icing/
Jun 21 05:09:06 Finished icing/                                               54m35s  25GB
Jun 21 05:09:07 Starting icing/examples
Jun 21 05:10:55 Finished icing/examples                                        1m47s   8GB
Jun 21 05:10:56 Starting compiler/repl
Jun 21 05:19:50 Finished compiler/repl                                         8m53s  10GB
Jun 21 05:19:51 Starting unverified/sexpr-bootstrap/x64/64
Jun 21 05:31:32 Finished unverified/sexpr-bootstrap/x64/64                    11m14s  16GB
Jun 21 05:31:33 Starting unverified/sexpr-bootstrap/x64/32
Jun 21 05:40:57 Finished unverified/sexpr-bootstrap/x64/32                     9m05s  15GB
Jun 21 05:40:58 Starting compiler/benchmarks
Jun 21 05:41:43 Finished compiler/benchmarks                                     44s 713MB
Jun 21 05:41:44 Starting compiler/bootstrap/compilation/x64/64
Jun 21 21:18:34 Finished compiler/bootstrap/compilation/x64/64             15h36m36s 215GB
Jun 21 21:18:35 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 21 21:39:29 Finished compiler/bootstrap/compilation/x64/64/proofs         20m53s  36GB
Jun 21 21:39:30 Starting compiler/bootstrap/compilation/x64/32
Jun 22 05:08:59 Finished compiler/bootstrap/compilation/x64/32              7h29m21s 150GB
Jun 22 05:09:00 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 22 05:12:40 Finished compiler/bootstrap/compilation/x64/32/proofs          3m38s  21GB
Jun 22 05:12:41 Starting compiler/bootstrap/compilation/ag32/32
Jun 22 13:31:10 Finished compiler/bootstrap/compilation/ag32/32             8h18m28s 180GB
Jun 22 13:31:11 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 22 13:38:49 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m36s  47GB
Jun 22 13:38:50 SUCCESS