Job 2397

CakeML:ba448b02f6dfebd0069315be9302ce9471b19ba4
  Fix for proofs broken by sublist in rich_listTheory [May 25 05:59:02]
HOL:19857c9570c4db45bb6410a1ced45b9ab7bb4cb7
  Fixed intLib to avoid noisy output; some cleanups in hurdUtils [May 22 11:23:37]
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

May 26 13:02:16 Claimed job
May 26 13:02:25 Building HOL
May 26 13:17:11 Starting developers
May 26 13:17:15 Finished developers                                               2s 173MB
May 26 13:17:16 Starting developers/bin
May 26 13:17:30 Finished developers/bin                                          13s   1GB
May 26 13:17:31 Starting compiler/proofs
May 26 15:13:16 Finished compiler/proofs                                    1h55m43s  52GB
May 26 15:13:17 Starting compiler/bootstrap/translation
May 26 23:16:38 Finished compiler/bootstrap/translation                     8h03m19s  71GB
May 26 23:16:38 Starting semantics/ffi
May 26 23:16:48 Finished semantics/ffi                                            8s 640MB
May 26 23:16:48 Starting semantics
May 26 23:16:50 Finished semantics                                                0s  67MB
May 26 23:16:51 Starting semantics/proofs
May 26 23:17:27 Finished semantics/proofs                                        35s   1GB
May 26 23:17:28 Starting semantics/alt_semantics
May 26 23:18:08 Finished semantics/alt_semantics                                 39s   1GB
May 26 23:18:09 Starting semantics/alt_semantics/proofs
May 26 23:29:56 Finished semantics/alt_semantics/proofs                       11m45s   5GB
May 26 23:29:57 Starting basis/pure
May 26 23:29:58 Finished basis/pure                                               0s  68MB
May 26 23:29:59 Starting translator
May 26 23:31:45 Finished translator                                            1m44s   4GB
May 26 23:31:45 Starting compiler/parsing
May 26 23:31:47 Finished compiler/parsing                                         0s  73MB
May 26 23:31:48 Starting characteristic
May 26 23:31:49 Finished characteristic                                           0s  89MB
May 26 23:31:50 Starting translator/monadic
May 26 23:31:52 Finished translator/monadic                                       0s  92MB
May 26 23:31:53 Starting basis
May 26 23:50:29 Finished basis                                                18m35s   5GB
May 26 23:50:30 Starting compiler/inference
May 26 23:50:32 Finished compiler/inference                                       0s  80MB
May 26 23:50:33 Starting compiler/backend/reg_alloc
May 26 23:50:34 Finished compiler/backend/reg_alloc                               0s  67MB
May 26 23:50:35 Starting compiler/backend/gc
May 26 23:50:37 Finished compiler/backend/gc                                      0s 138MB
May 26 23:50:38 Starting compiler/backend
May 26 23:50:58 Finished compiler/backend                                        18s   1GB
May 26 23:50:58 Starting compiler/encoders/asm
May 26 23:51:00 Finished compiler/encoders/asm                                    0s  93MB
May 26 23:51:01 Starting compiler/encoders/x64
May 26 23:51:02 Finished compiler/encoders/x64                                    0s 103MB
May 26 23:51:03 Starting compiler/encoders/arm7
May 26 23:51:05 Finished compiler/encoders/arm7                                   0s 105MB
May 26 23:51:06 Starting compiler/encoders/arm8
May 26 23:51:07 Finished compiler/encoders/arm8                                   0s 105MB
May 26 23:51:08 Starting compiler/encoders/arm8_asl
May 27 02:04:31 Finished compiler/encoders/arm8_asl                         2h13m21s  41GB
May 27 02:04:32 Starting compiler/encoders/mips
May 27 02:04:33 Finished compiler/encoders/mips                                   0s 103MB
May 27 02:04:35 Starting compiler/encoders/riscv
May 27 02:04:36 Finished compiler/encoders/riscv                                  0s  94MB
May 27 02:04:37 Starting compiler/encoders/ag32
May 27 02:04:39 Finished compiler/encoders/ag32                                   0s  92MB
May 27 02:04:40 Starting compiler/backend/x64
May 27 02:04:41 Finished compiler/backend/x64                                     0s 136MB
May 27 02:04:42 Starting compiler/backend/arm7
May 27 02:04:44 Finished compiler/backend/arm7                                    0s 136MB
May 27 02:04:45 Starting compiler/backend/arm8
May 27 02:04:47 Finished compiler/backend/arm8                                    0s 136MB
May 27 02:04:48 Starting compiler/backend/mips
May 27 02:04:50 Finished compiler/backend/mips                                    0s 136MB
May 27 02:04:51 Starting compiler/backend/riscv
May 27 02:04:52 Finished compiler/backend/riscv                                   0s 136MB
May 27 02:04:53 Starting compiler/backend/ag32
May 27 02:06:13 Finished compiler/backend/ag32                                 1m19s   2GB
May 27 02:06:14 Starting compiler/parsing/proofs
May 27 02:06:16 Finished compiler/parsing/proofs                                  0s  74MB
May 27 02:06:17 Starting compiler/inference/proofs
May 27 02:06:18 Finished compiler/inference/proofs                                0s  88MB
May 27 02:06:19 Starting compiler/backend/semantics
May 27 02:10:04 Finished compiler/backend/semantics                            3m43s   4GB
May 27 02:10:05 Starting compiler/backend/reg_alloc/proofs
May 27 02:10:06 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
May 27 02:10:07 Starting compiler/backend/proofs
May 27 02:11:14 Finished compiler/backend/proofs                               1m06s   3GB
May 27 02:11:16 Starting compiler/backend/serialiser
May 27 02:11:18 Finished compiler/backend/serialiser                              1s 201MB
May 27 02:11:19 Starting compiler/encoders/x64/proofs
May 27 02:20:42 Finished compiler/encoders/x64/proofs                          9m21s   5GB
May 27 02:20:43 Starting compiler/encoders/arm7/proofs
May 27 02:33:35 Finished compiler/encoders/arm7/proofs                        12m50s  11GB
May 27 02:33:36 Starting compiler/encoders/arm8/proofs
May 27 02:40:09 Finished compiler/encoders/arm8/proofs                         6m31s   5GB
May 27 02:40:10 Starting compiler/encoders/arm8_asl/proofs
May 27 03:27:36 Finished compiler/encoders/arm8_asl/proofs                    47m25s   6GB
May 27 03:27:36 Starting compiler/encoders/mips/proofs
May 27 03:37:52 Finished compiler/encoders/mips/proofs                        10m14s   9GB
May 27 03:37:53 Starting compiler/encoders/riscv/proofs
May 27 03:46:21 Finished compiler/encoders/riscv/proofs                        8m27s   5GB
May 27 03:46:22 Starting compiler/encoders/ag32/proofs
May 27 03:48:46 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
May 27 03:48:47 Starting compiler/backend/x64/proofs
May 27 03:49:30 Finished compiler/backend/x64/proofs                             42s   3GB
May 27 03:49:31 Starting compiler/backend/arm7/proofs
May 27 03:50:18 Finished compiler/backend/arm7/proofs                            45s   2GB
May 27 03:50:19 Starting compiler/backend/arm8/proofs
May 27 03:51:03 Finished compiler/backend/arm8/proofs                            42s   3GB
May 27 03:51:04 Starting compiler/backend/arm8_asl
May 27 03:51:33 Finished compiler/backend/arm8_asl                               28s   2GB
May 27 03:51:34 Starting compiler/backend/mips/proofs
May 27 03:52:22 Finished compiler/backend/mips/proofs                            46s   3GB
May 27 03:52:23 Starting compiler/backend/riscv/proofs
May 27 03:53:15 Finished compiler/backend/riscv/proofs                           51s   4GB
May 27 03:53:16 Starting compiler/backend/ag32/proofs
May 27 04:07:10 Finished compiler/backend/ag32/proofs                         13m53s   6GB
May 27 04:07:11 Starting candle/set-theory
May 27 04:08:00 Finished candle/set-theory                                       48s   1GB
May 27 04:08:01 Starting candle/syntax-lib
May 27 04:08:02 Finished candle/syntax-lib                                        0s  73MB
May 27 04:08:03 Starting candle/standard/syntax
May 27 04:08:22 Finished candle/standard/syntax                                  17s   1GB
May 27 04:08:23 Starting candle/standard/semantics
May 27 04:11:01 Finished candle/standard/semantics                             2m36s   3GB
May 27 04:11:02 Starting candle/standard/monadic
May 27 04:11:03 Finished candle/standard/monadic                                  0s 103MB
May 27 04:11:04 Starting candle/standard/ml_kernel
May 27 04:12:58 Finished candle/standard/ml_kernel                             1m52s   6GB
May 27 04:12:59 Starting candle/overloading/syntax
May 27 04:16:33 Finished candle/overloading/syntax                             3m33s   2GB
May 27 04:16:34 Starting candle/overloading/semantics
May 27 04:28:08 Finished candle/overloading/semantics                         11m32s   5GB
May 27 04:28:09 Starting candle/overloading/monadic
May 27 04:30:44 Finished candle/overloading/monadic                            2m34s   2GB
May 27 04:30:45 Starting candle/overloading/ml_kernel
May 27 04:38:26 Finished candle/overloading/ml_kernel                          7m39s   7GB
May 27 04:38:27 Starting candle/overloading/ml_checker
May 27 04:41:02 Finished candle/overloading/ml_checker                         2m34s   6GB
May 27 04:41:03 Starting candle/prover
May 27 04:51:09 Finished candle/prover                                        10m05s   5GB
May 27 04:51:10 Starting pancake
May 27 04:52:20 Finished pancake                                               1m08s   1GB
May 27 04:52:20 Starting pancake/ffi
May 27 04:52:21 Finished pancake/ffi                                              0s  21MB
May 27 04:52:22 Starting pancake/semantics
May 27 04:55:06 Finished pancake/semantics                                     2m43s   2GB
May 27 04:55:07 Starting pancake/parser
May 27 04:55:39 Finished pancake/parser                                          30s   2GB
May 27 04:55:40 Starting pancake/proofs
May 27 05:26:44 Finished pancake/proofs                                       31m02s  11GB
May 27 05:26:44 Starting characteristic/examples
May 27 05:28:20 Finished characteristic/examples                               1m35s   6GB
May 27 05:28:21 Starting tutorial/solutions
May 27 05:44:07 Finished tutorial/solutions                                   15m44s  13GB
May 27 05:44:07 Starting translator/monadic/examples
May 27 05:48:08 Finished translator/monadic/examples                           3m59s   5GB
May 27 05:48:09 Starting examples
May 27 06:02:52 Finished examples                                             14m42s   8GB
May 27 06:02:53 Starting examples/compilation/x64
May 27 08:01:45 Finished examples/compilation/x64                           1h58m50s  39GB
May 27 08:01:46 Starting examples/compilation/x64/proofs
May 27 08:05:43 Finished examples/compilation/x64/proofs                       3m56s   6GB
May 27 08:05:44 Starting examples/compilation/ag32
May 27 08:36:48 Finished examples/compilation/ag32                            31m03s  13GB
May 27 08:36:49 Starting examples/compilation/ag32/proofs
May 27 08:38:18 Finished examples/compilation/ag32/proofs                      1m27s   7GB
May 27 08:38:19 Starting examples/compilation/to_word
May 27 08:42:24 Finished examples/compilation/to_word                          4m04s  14GB
May 27 08:42:25 Starting examples/lpr_checker
May 27 08:43:46 Finished examples/lpr_checker                                  1m20s   2GB
May 27 08:43:47 Starting examples/lpr_checker/array
May 27 09:12:22 Finished examples/lpr_checker/array                           28m33s  11GB
May 27 09:12:23 Starting examples/lpr_checker/array/compilation
May 27 09:51:58 Finished examples/lpr_checker/array/compilation               39m33s  67GB
May 27 09:51:59 Starting examples/lpr_checker/array/compilation/proofs
May 27 09:53:43 Finished examples/lpr_checker/array/compilation/proofs         1m43s   8GB
May 27 09:53:44 Starting examples/lpr_checker/array/compilation/proofsARM8
May 27 10:05:21 Finished examples/lpr_checker/array/compilation/proofsARM8    11m36s  33GB
May 27 10:05:22 Starting examples/xlrup_checker
May 27 10:06:34 Finished examples/xlrup_checker                                1m11s   2GB
May 27 10:06:35 Starting examples/xlrup_checker/array
May 27 10:21:36 Finished examples/xlrup_checker/array                         15m00s   8GB
May 27 10:21:37 Starting examples/xlrup_checker/array/compilation
May 27 10:43:29 Finished examples/xlrup_checker/array/compilation             21m50s  35GB
May 27 10:43:30 Starting examples/xlrup_checker/array/compilation/proofs
May 27 10:45:00 Finished examples/xlrup_checker/array/compilation/proofs       1m29s   7GB
May 27 10:45:01 Starting examples/pseudo_bool
May 27 10:47:12 Finished examples/pseudo_bool                                  2m10s   2GB
May 27 10:47:13 Starting examples/pseudo_bool/cnf_encoding
May 27 10:47:53 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
May 27 10:47:54 Starting examples/pseudo_bool/graph_encoding
May 27 10:48:48 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
May 27 10:48:49 Starting examples/pseudo_bool/array
May 27 11:55:21 Finished examples/pseudo_bool/array                         1h06m30s  43GB
May 27 11:55:22 Starting examples/pseudo_bool/array/compilation
May 27 19:50:14 Finished examples/pseudo_bool/array/compilation             7h54m50s 145GB
May 27 19:50:15 Starting examples/pseudo_bool/array/compilation/proofs
May 27 19:53:37 Finished examples/pseudo_bool/array/compilation/proofs         3m20s   8GB
May 27 19:53:38 Starting examples/opentheory
May 27 20:04:25 Finished examples/opentheory                                  10m46s   7GB
May 27 20:04:26 Starting examples/opentheory
May 27 20:04:28 Finished examples/opentheory                                      0s 126MB
May 27 20:04:29 Starting examples/opentheory/compilation
May 27 20:41:05 Finished examples/opentheory/compilation                      36m35s  54GB
May 27 20:41:06 Starting examples/opentheory/compilation/proofs
May 27 20:42:43 Finished examples/opentheory/compilation/proofs                1m35s   6GB
May 27 20:42:44 Starting examples/opentheory/compilation/ag32
May 27 21:17:13 Finished examples/opentheory/compilation/ag32                 34m27s  66GB
May 27 21:17:14 Starting examples/opentheory/compilation/ag32/proofs
May 27 21:19:36 Finished examples/opentheory/compilation/ag32/proofs           2m21s  11GB
May 27 21:19:37 Starting examples/sat_encodings
May 27 21:22:36 Finished examples/sat_encodings                                2m58s   2GB
May 27 21:22:37 Starting examples/sat_encodings/case_studies
May 27 21:24:43 Finished examples/sat_encodings/case_studies                   2m05s   2GB
May 27 21:24:44 Starting examples/sat_encodings/translation
May 27 21:31:05 Finished examples/sat_encodings/translation                    6m19s   7GB
May 27 21:31:06 Starting examples/sat_encodings/translation/compilation
May 27 22:05:54 Finished examples/sat_encodings/translation/compilation       34m47s  35GB
May 27 22:05:55 Starting examples/deflate
May 27 22:07:18 Finished examples/deflate                                      1m22s   1GB
May 27 22:07:19 Starting examples/deflate/translation
May 27 22:09:02 Finished examples/deflate/translation                          1m41s   7GB
May 27 22:09:03 Starting examples/deflate/translation/compilation
May 27 22:26:05 Finished examples/deflate/translation/compilation             17m01s  30GB
May 27 22:26:06 Starting examples/vipr
May 27 22:30:16 Finished examples/vipr                                         4m08s   7GB
May 27 22:30:17 Starting examples/vipr/compilation
May 27 22:50:32 Finished examples/vipr/compilation                            20m14s  39GB
May 27 22:50:33 Starting translator/okasaki-examples
May 27 22:55:45 Finished translator/okasaki-examples                           5m10s   4GB
May 27 22:55:45 Starting translator/other-examples
May 27 23:00:45 Finished translator/other-examples                             4m58s   3GB
May 27 23:00:46 Starting compiler/parsing/tests
May 27 23:01:21 Finished compiler/parsing/tests                                  33s   2GB
May 27 23:01:22 Starting compiler/inference/tests
May 27 23:08:47 Finished compiler/inference/tests                              7m24s   6GB
May 27 23:08:48 Starting compiler/printing/test
May 27 23:12:20 Finished compiler/printing/test                                3m31s   6GB
May 27 23:12:21 Starting icing/flover
May 27 23:50:32 Finished icing/flover                                         38m09s   4GB
May 27 23:50:33 Starting icing/
May 28 00:46:35 Finished icing/                                               56m01s  28GB
May 28 00:46:36 Starting icing/examples
May 28 00:48:20 Finished icing/examples                                        1m42s   9GB
May 28 00:48:21 Starting compiler/repl
May 28 00:57:10 Finished compiler/repl                                         8m48s   8GB
May 28 00:57:11 Starting unverified/sexpr-bootstrap/x64/64
May 28 01:08:40 Finished unverified/sexpr-bootstrap/x64/64                    11m03s  16GB
May 28 01:08:41 Starting unverified/sexpr-bootstrap/x64/32
May 28 01:17:58 Finished unverified/sexpr-bootstrap/x64/32                     8m55s  13GB
May 28 01:17:59 Starting compiler/benchmarks
May 28 01:18:44 Finished compiler/benchmarks                                     44s 713MB
May 28 01:18:45 Starting compiler/bootstrap/compilation/x64/64
May 28 16:48:16 Finished compiler/bootstrap/compilation/x64/64             15h29m18s 175GB
May 28 16:48:17 Starting compiler/bootstrap/compilation/x64/64/proofs
May 28 17:09:40 Finished compiler/bootstrap/compilation/x64/64/proofs         21m22s  48GB
May 28 17:09:41 Starting compiler/bootstrap/compilation/x64/32
May 29 01:02:33 Finished compiler/bootstrap/compilation/x64/32              7h52m44s 205GB
May 29 01:02:34 Starting compiler/bootstrap/compilation/x64/32/proofs
May 29 01:06:16 Finished compiler/bootstrap/compilation/x64/32/proofs          3m40s  19GB
May 29 01:06:16 Starting compiler/bootstrap/compilation/ag32/32
May 29 08:57:14 Finished compiler/bootstrap/compilation/ag32/32             7h50m56s 154GB
May 29 08:57:15 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 29 09:05:20 Finished compiler/bootstrap/compilation/ag32/32/proofs         8m04s  51GB
May 29 09:05:21 SUCCESS