Job 1685

CakeML:ac6dd83f48ab211455fb85c60d3e20e212dc7b8a
  Remove some primes [Dec 12 21:27:55]
HOL:c51de550191d516cb9dfe47c6a1e866b232f2c96
  Remove another use of .. that causes grammar precedence problems [Dec 09 23:13:20]
Machine:oven3 4.19.67.1.amd64-smp
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Dec 12 21:42:23 Claimed job
Dec 12 21:42:41 Building HOL
Dec 12 22:02:11 Starting developers
Dec 12 22:02:19 Finished developers                                               8s 106MB
Dec 12 22:02:19 Starting developers/bin
Dec 12 22:02:34 Finished developers/bin                                          12s   1GB
Dec 12 22:02:34 Starting semantics/ffi
Dec 12 22:02:53 Finished semantics/ffi                                           18s 248MB
Dec 12 22:02:53 Starting semantics
Dec 12 22:06:05 Finished semantics                                             3m11s   1GB
Dec 12 22:06:05 Starting semantics/proofs
Dec 12 22:14:03 Finished semantics/proofs                                      7m57s   1GB
Dec 12 22:14:03 Starting semantics/alt_semantics
Dec 12 22:14:28 Finished semantics/alt_semantics                                 24s 442MB
Dec 12 22:14:28 Starting semantics/alt_semantics/proofs
Dec 12 22:19:33 Finished semantics/alt_semantics/proofs                        5m04s   1GB
Dec 12 22:19:33 Starting basis/pure
Dec 12 22:25:51 Finished basis/pure                                            6m17s 822MB
Dec 12 22:25:51 Starting translator
Dec 12 22:31:42 Finished translator                                            5m50s   1GB
Dec 12 22:31:42 Starting compiler/parsing
Dec 12 22:34:20 Finished compiler/parsing                                      2m37s   2GB
Dec 12 22:34:20 Starting characteristic
Dec 12 22:46:22 Finished characteristic                                       12m02s   1GB
Dec 12 22:46:23 Starting translator/monadic
Dec 12 22:49:50 Finished translator/monadic                                    3m26s   1GB
Dec 12 22:49:50 Starting basis
Dec 13 00:27:51 Finished basis                                              1h38m01s  14GB
Dec 13 00:27:51 Starting compiler/inference
Dec 13 00:30:34 Finished compiler/inference                                    2m42s   1GB
Dec 13 00:30:34 Starting compiler/backend/reg_alloc
Dec 13 00:32:38 Finished compiler/backend/reg_alloc                            2m03s   1GB
Dec 13 00:32:38 Starting compiler/backend/gc
Dec 13 00:39:28 Finished compiler/backend/gc                                   6m49s   2GB
Dec 13 00:39:29 Starting compiler/backend
Dec 13 00:48:15 Finished compiler/backend                                      8m45s   2GB
Dec 13 00:48:15 Starting compiler/encoders/asm
Dec 13 00:49:04 Finished compiler/encoders/asm                                   48s 697MB
Dec 13 00:49:04 Starting compiler/encoders/x64
Dec 13 00:51:24 Finished compiler/encoders/x64                                 2m19s 683MB
Dec 13 00:51:24 Starting compiler/encoders/arm7
Dec 13 00:55:45 Finished compiler/encoders/arm7                                4m21s   1GB
Dec 13 00:55:45 Starting compiler/encoders/arm8
Dec 13 00:57:06 Finished compiler/encoders/arm8                                1m20s 908MB
Dec 13 00:57:06 Starting compiler/encoders/mips
Dec 13 01:00:11 Finished compiler/encoders/mips                                3m05s   1GB
Dec 13 01:00:12 Starting compiler/encoders/riscv
Dec 13 01:03:55 Finished compiler/encoders/riscv                               3m42s   1GB
Dec 13 01:03:55 Starting compiler/encoders/ag32
Dec 13 01:04:37 Finished compiler/encoders/ag32                                  41s 660MB
Dec 13 01:04:37 Starting compiler/backend/x64
Dec 13 01:05:20 Finished compiler/backend/x64                                    42s   1GB
Dec 13 01:05:20 Starting compiler/backend/arm7
Dec 13 01:06:06 Finished compiler/backend/arm7                                   46s   1GB
Dec 13 01:06:06 Starting compiler/backend/arm8
Dec 13 01:06:50 Finished compiler/backend/arm8                                   43s   1GB
Dec 13 01:06:50 Starting compiler/backend/mips
Dec 13 01:07:29 Finished compiler/backend/mips                                   39s   1GB
Dec 13 01:07:30 Starting compiler/backend/riscv
Dec 13 01:08:11 Finished compiler/backend/riscv                                  40s   1GB
Dec 13 01:08:11 Starting compiler/backend/ag32
Dec 13 01:10:39 Finished compiler/backend/ag32                                 2m27s   1GB
Dec 13 01:10:39 Starting compiler/parsing/proofs
Dec 13 01:18:59 Finished compiler/parsing/proofs                               8m20s   1GB
Dec 13 01:18:59 Starting compiler/inference/proofs
Dec 13 01:24:26 Finished compiler/inference/proofs                             5m26s 929MB
Dec 13 01:24:26 Starting compiler/backend/semantics
Dec 13 02:26:08 Finished compiler/backend/semantics                         1h01m41s   3GB
Dec 13 02:26:09 Starting compiler/backend/reg_alloc/proofs
Dec 13 02:33:43 Finished compiler/backend/reg_alloc/proofs                     7m34s 826MB
Dec 13 02:33:43 Starting compiler/backend/proofs
Dec 13 04:13:50 Finished compiler/backend/proofs                            1h40m06s  15GB
Dec 13 04:13:51 Starting compiler/backend/serialiser
Dec 13 04:16:19 Finished compiler/backend/serialiser                           2m28s   2GB
Dec 13 04:16:20 Starting compiler/encoders/x64/proofs
Dec 13 04:37:48 Finished compiler/encoders/x64/proofs                         21m28s   6GB
Dec 13 04:37:48 Starting compiler/encoders/arm7/proofs
Dec 13 05:06:58 Finished compiler/encoders/arm7/proofs                        29m09s   3GB
Dec 13 05:06:58 Starting compiler/encoders/arm8/proofs
Dec 13 05:22:29 Finished compiler/encoders/arm8/proofs                        15m29s   1GB
Dec 13 05:22:29 Starting compiler/encoders/mips/proofs
Dec 13 05:45:02 Finished compiler/encoders/mips/proofs                        22m33s   2GB
Dec 13 05:45:02 Starting compiler/encoders/riscv/proofs
Dec 13 06:05:04 Finished compiler/encoders/riscv/proofs                       20m01s   1GB
Dec 13 06:05:04 Starting compiler/encoders/ag32/proofs
Dec 13 06:10:43 Finished compiler/encoders/ag32/proofs                         5m38s 844MB
Dec 13 06:10:43 Starting compiler/backend/x64/proofs
Dec 13 06:11:32 Finished compiler/backend/x64/proofs                             48s   1GB
Dec 13 06:11:32 Starting compiler/backend/arm7/proofs
Dec 13 06:12:23 Finished compiler/backend/arm7/proofs                            50s   1GB
Dec 13 06:12:23 Starting compiler/backend/arm8/proofs
Dec 13 06:13:22 Finished compiler/backend/arm8/proofs                            58s 972MB
Dec 13 06:13:22 Starting compiler/backend/mips/proofs
Dec 13 06:14:12 Finished compiler/backend/mips/proofs                            49s   1GB
Dec 13 06:14:12 Starting compiler/backend/riscv/proofs
Dec 13 06:15:04 Finished compiler/backend/riscv/proofs                           51s   1GB
Dec 13 06:15:04 Starting compiler/backend/ag32/proofs
Dec 13 06:42:56 Finished compiler/backend/ag32/proofs                         27m51s   2GB
Dec 13 06:42:56 Starting compiler/proofs
Dec 13 06:47:01 Finished compiler/proofs                                       4m05s   2GB
Dec 13 06:47:02 Starting candle/set-theory
Dec 13 06:47:59 Finished candle/set-theory                                       57s 696MB
Dec 13 06:47:59 Starting candle/syntax-lib
Dec 13 06:48:23 Finished candle/syntax-lib                                       23s 497MB
Dec 13 06:48:23 Starting candle/standard/syntax
Dec 13 06:52:11 Finished candle/standard/syntax                                3m47s   1GB
Dec 13 06:52:12 Starting candle/standard/semantics
Dec 13 06:55:53 Finished candle/standard/semantics                             3m41s   1GB
Dec 13 06:55:53 Starting candle/standard/monadic
Dec 13 06:59:38 Finished candle/standard/monadic                               3m44s   1GB
Dec 13 06:59:39 Starting candle/standard/ml_kernel
Dec 13 07:11:05 Finished candle/standard/ml_kernel                            11m25s   3GB
Dec 13 07:11:05 Starting candle/overloading/syntax
Dec 13 07:17:28 Finished candle/overloading/syntax                             6m22s   1GB
Dec 13 07:17:28 Starting candle/overloading/semantics
Dec 13 07:42:29 Finished candle/overloading/semantics                         25m01s   2GB
Dec 13 07:42:30 Starting pancake
Dec 13 07:46:27 Finished pancake                                               3m57s   2GB
Dec 13 07:46:28 Starting pancake/ffi
Dec 13 07:46:28 Finished pancake/ffi                                              0s   7MB
Dec 13 07:46:28 Starting pancake/semantics
Dec 13 07:51:20 Finished pancake/semantics                                     4m51s   1GB
Dec 13 07:51:20 Starting pancake/proofs
Dec 13 08:16:38 Finished pancake/proofs                                       25m17s   5GB
Dec 13 08:16:38 Starting characteristic/examples
Dec 13 08:19:35 Finished characteristic/examples                               2m57s   3GB
Dec 13 08:19:36 Starting tutorial/solutions
Dec 13 08:54:44 Finished tutorial/solutions                                   35m07s  10GB
Dec 13 08:54:44 Starting translator/monadic/examples
Dec 13 09:00:23 Finished translator/monadic/examples                           5m38s   2GB
Dec 13 09:00:23 Starting examples
Dec 13 09:18:14 Finished examples                                             17m50s   3GB
Dec 13 09:18:14 Starting examples/compilation/x64
Dec 13 14:48:30 Finished examples/compilation/x64                           5h30m15s  29GB
Dec 13 14:48:30 Starting examples/compilation/x64/proofs
Dec 13 14:52:07 Finished examples/compilation/x64/proofs                       3m36s   3GB
Dec 13 14:52:07 Starting examples/compilation/ag32
Dec 13 16:09:09 Finished examples/compilation/ag32                          1h17m01s  10GB
Dec 13 16:09:09 Starting examples/compilation/ag32/proofs
Dec 13 16:10:43 Finished examples/compilation/ag32/proofs                      1m32s   3GB
Dec 13 16:10:43 Starting examples/cost
Dec 13 18:07:09 Finished examples/cost                                      1h56m26s   7GB
Dec 13 18:07:10 Starting examples/lpr_checker
Dec 13 18:08:50 Finished examples/lpr_checker                                  1m40s   1GB
Dec 13 18:08:50 Starting examples/lpr_checker/array
Dec 13 19:11:48 Finished examples/lpr_checker/array                         1h02m57s   6GB
Dec 13 19:11:49 Starting examples/lpr_checker/array/compilation
Dec 13 22:12:12 Finished examples/lpr_checker/array/compilation             3h00m22s  36GB
Dec 13 22:12:12 Starting examples/lpr_checker/array/compilation/proofs
Dec 13 22:14:46 Finished examples/lpr_checker/array/compilation/proofs         2m33s   7GB
Dec 13 22:14:46 Starting examples/opentheory
Dec 13 22:35:16 Finished examples/opentheory                                  20m29s   6GB
Dec 13 22:35:16 Starting examples/opentheory
Dec 13 22:35:19 Finished examples/opentheory                                      2s  33MB
Dec 13 22:35:19 Starting examples/opentheory/compilation
Dec 13 23:57:49 Finished examples/opentheory/compilation                    1h22m29s  41GB
Dec 13 23:57:50 Starting examples/opentheory/compilation/proofs
Dec 13 23:59:21 Finished examples/opentheory/compilation/proofs                1m31s   4GB
Dec 13 23:59:21 Starting examples/opentheory/compilation/ag32
Dec 14 01:24:45 Finished examples/opentheory/compilation/ag32               1h25m22s  35GB
Dec 14 01:24:45 Starting examples/opentheory/compilation/ag32/proofs
Dec 14 01:28:17 Finished examples/opentheory/compilation/ag32/proofs           3m32s   6GB
Dec 14 01:28:18 Starting examples/sat_encodings
Dec 14 01:32:03 Finished examples/sat_encodings                                3m45s   1GB
Dec 14 01:32:03 Starting examples/sat_encodings/case_studies
Dec 14 01:35:22 Finished examples/sat_encodings/case_studies                   3m18s 983MB
Dec 14 01:35:22 Starting examples/sat_encodings/translation
Dec 14 01:47:07 Finished examples/sat_encodings/translation                   11m45s   3GB
Dec 14 01:47:08 Starting examples/sat_encodings/translation/compilation
Dec 14 03:14:14 Finished examples/sat_encodings/translation/compilation     1h27m04s  29GB
Dec 14 03:14:14 Starting translator/okasaki-examples
Dec 14 03:23:30 Finished translator/okasaki-examples                           9m16s   2GB
Dec 14 03:23:31 Starting translator/other-examples
Dec 14 03:27:04 Finished translator/other-examples                             3m33s   1GB
Dec 14 03:27:05 Starting compiler/parsing/tests
Dec 14 03:28:12 Finished compiler/parsing/tests                                1m06s 503MB
Dec 14 03:28:12 Starting compiler/inference/tests
Dec 14 03:44:29 Finished compiler/inference/tests                             16m17s   5GB
Dec 14 03:44:30 Starting compiler/bootstrap/translation
Dec 14 09:16:03 Finished compiler/bootstrap/translation                     5h31m31s  31GB
Dec 14 09:16:03 Starting unverified/sexpr-bootstrap/x64/64
Dec 14 09:40:19 Finished unverified/sexpr-bootstrap/x64/64                    24m11s  10GB
Dec 14 09:40:19 Starting unverified/sexpr-bootstrap/x64/32
Dec 14 10:01:15 Finished unverified/sexpr-bootstrap/x64/32                    20m51s   8GB
Dec 14 10:01:15 Starting compiler/benchmarks
Dec 14 10:01:20 Finished compiler/benchmarks                                      4s  34MB
Dec 14 10:01:20 Starting compiler/bootstrap/compilation/x64/64
Dec 15 15:25:17 Finished compiler/bootstrap/compilation/x64/64             29h23m52s 113GB
Dec 15 15:25:18 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 15 15:30:12 Finished compiler/bootstrap/compilation/x64/64/proofs          4m54s  16GB
Dec 15 15:30:12 Starting compiler/bootstrap/compilation/x64/32
Dec 21 06:34:10 Resuming compiler/bootstrap/compilation/x64/32
Dec 21 06:34:20 Finished compiler/bootstrap/compilation/x64/32                    7s  30MB
Dec 21 06:34:20 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 21 06:38:32 Finished compiler/bootstrap/compilation/x64/32/proofs          4m11s  14GB
Dec 21 06:38:32 Starting compiler/bootstrap/compilation/ag32/32
Dec 22 07:33:18 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++89684.70+102736716
Dec 22 07:33:18 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Dec 22 07:53:04 Finished+compiler/bootstrap/compilation/ag32/32/proofs+++++1185.08+38783288
Dec 22 07:53:04 SUCCESS