Job 2270

CakeML:45534e558612704f938386fc12b79bc991c3afa3
  Update for new year [Jan 01 02:20:21]
HOL:fbdc8f631085370c871c50b58817d2e5b679eb88
  Reverted [REC]; re-worked REC_VAR_NO_TRANS (and I_NO_TRANS) by method [Jan 11 22:08:58]
Machine:pavlova
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 15 14:45:31 Claimed job
Jan 15 14:45:37 Building HOL
Jan 15 15:00:25 Starting developers
Jan 15 15:00:29 Finished developers                                               2s 219MB
Jan 15 15:00:30 Starting developers/bin
Jan 15 15:00:40 Finished developers/bin                                           9s   1GB
Jan 15 15:00:41 Starting compiler/proofs
Jan 15 16:45:21 Finished compiler/proofs                                    1h44m39s  32GB
Jan 15 16:45:22 Starting compiler/bootstrap/translation
Jan 16 00:42:49 Finished compiler/bootstrap/translation                     7h57m26s  75GB
Jan 16 00:42:50 Starting semantics/ffi
Jan 16 00:42:59 Finished semantics/ffi                                            7s 578MB
Jan 16 00:43:00 Starting semantics
Jan 16 00:43:01 Finished semantics                                                0s  66MB
Jan 16 00:43:02 Starting semantics/proofs
Jan 16 00:43:37 Finished semantics/proofs                                        33s   2GB
Jan 16 00:43:38 Starting semantics/alt_semantics
Jan 16 00:44:17 Finished semantics/alt_semantics                                 38s   1GB
Jan 16 00:44:18 Starting semantics/alt_semantics/proofs
Jan 16 00:55:14 Finished semantics/alt_semantics/proofs                       10m54s   5GB
Jan 16 00:55:15 Starting basis/pure
Jan 16 00:55:16 Finished basis/pure                                               0s  66MB
Jan 16 00:55:17 Starting translator
Jan 16 00:56:59 Finished translator                                            1m41s   4GB
Jan 16 00:57:00 Starting compiler/parsing
Jan 16 00:57:01 Finished compiler/parsing                                         0s  72MB
Jan 16 00:57:02 Starting characteristic
Jan 16 00:57:04 Finished characteristic                                           0s  93MB
Jan 16 00:57:04 Starting translator/monadic
Jan 16 00:57:06 Finished translator/monadic                                       0s  99MB
Jan 16 00:57:07 Starting basis
Jan 16 01:00:43 Finished basis                                                 3m34s   5GB
Jan 16 01:00:43 Starting compiler/inference
Jan 16 01:00:45 Finished compiler/inference                                       0s  85MB
Jan 16 01:00:46 Starting compiler/backend/reg_alloc
Jan 16 01:00:47 Finished compiler/backend/reg_alloc                               0s  66MB
Jan 16 01:00:48 Starting compiler/backend/gc
Jan 16 01:00:50 Finished compiler/backend/gc                                      0s 138MB
Jan 16 01:00:50 Starting compiler/backend
Jan 16 01:01:08 Finished compiler/backend                                        16s   1GB
Jan 16 01:01:09 Starting compiler/encoders/asm
Jan 16 01:01:10 Finished compiler/encoders/asm                                    0s  91MB
Jan 16 01:01:11 Starting compiler/encoders/x64
Jan 16 01:01:13 Finished compiler/encoders/x64                                    0s  94MB
Jan 16 01:01:13 Starting compiler/encoders/arm7
Jan 16 01:01:15 Finished compiler/encoders/arm7                                   0s  95MB
Jan 16 01:01:16 Starting compiler/encoders/arm8
Jan 16 01:01:17 Finished compiler/encoders/arm8                                   0s  91MB
Jan 16 01:01:18 Starting compiler/encoders/arm8_asl
Jan 16 03:09:23 Finished compiler/encoders/arm8_asl                         2h08m03s  44GB
Jan 16 03:09:24 Starting compiler/encoders/mips
Jan 16 03:09:25 Finished compiler/encoders/mips                                   0s  87MB
Jan 16 03:09:26 Starting compiler/encoders/riscv
Jan 16 03:09:28 Finished compiler/encoders/riscv                                  0s  88MB
Jan 16 03:09:29 Starting compiler/encoders/ag32
Jan 16 03:09:30 Finished compiler/encoders/ag32                                   0s  85MB
Jan 16 03:09:31 Starting compiler/backend/x64
Jan 16 03:09:32 Finished compiler/backend/x64                                     0s 129MB
Jan 16 03:09:33 Starting compiler/backend/arm7
Jan 16 03:09:35 Finished compiler/backend/arm7                                    0s 129MB
Jan 16 03:09:36 Starting compiler/backend/arm8
Jan 16 03:09:38 Finished compiler/backend/arm8                                    0s 129MB
Jan 16 03:09:38 Starting compiler/backend/mips
Jan 16 03:09:40 Finished compiler/backend/mips                                    0s 129MB
Jan 16 03:09:41 Starting compiler/backend/riscv
Jan 16 03:09:43 Finished compiler/backend/riscv                                   0s 129MB
Jan 16 03:09:43 Starting compiler/backend/ag32
Jan 16 03:11:02 Finished compiler/backend/ag32                                 1m17s   3GB
Jan 16 03:11:02 Starting compiler/parsing/proofs
Jan 16 03:11:04 Finished compiler/parsing/proofs                                  0s  75MB
Jan 16 03:11:05 Starting compiler/inference/proofs
Jan 16 03:11:06 Finished compiler/inference/proofs                                0s  86MB
Jan 16 03:11:07 Starting compiler/backend/semantics
Jan 16 03:12:34 Finished compiler/backend/semantics                            1m25s   2GB
Jan 16 03:12:35 Starting compiler/backend/reg_alloc/proofs
Jan 16 03:12:36 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jan 16 03:12:37 Starting compiler/backend/proofs
Jan 16 03:13:40 Finished compiler/backend/proofs                               1m02s   4GB
Jan 16 03:13:41 Starting compiler/backend/serialiser
Jan 16 03:13:43 Finished compiler/backend/serialiser                              1s 188MB
Jan 16 03:13:44 Starting compiler/encoders/x64/proofs
Jan 16 03:23:09 Finished compiler/encoders/x64/proofs                          9m23s   5GB
Jan 16 03:23:10 Starting compiler/encoders/arm7/proofs
Jan 16 03:35:59 Finished compiler/encoders/arm7/proofs                        12m48s  11GB
Jan 16 03:36:00 Starting compiler/encoders/arm8/proofs
Jan 16 03:42:37 Finished compiler/encoders/arm8/proofs                         6m36s   5GB
Jan 16 03:42:38 Starting compiler/encoders/arm8_asl/proofs
Jan 16 04:30:27 Finished compiler/encoders/arm8_asl/proofs                    47m47s  10GB
Jan 16 04:30:28 Starting compiler/encoders/mips/proofs
Jan 16 04:40:32 Finished compiler/encoders/mips/proofs                        10m03s   7GB
Jan 16 04:40:33 Starting compiler/encoders/riscv/proofs
Jan 16 04:48:39 Finished compiler/encoders/riscv/proofs                        8m04s   3GB
Jan 16 04:48:40 Starting compiler/encoders/ag32/proofs
Jan 16 04:51:02 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Jan 16 04:51:03 Starting compiler/backend/x64/proofs
Jan 16 04:51:43 Finished compiler/backend/x64/proofs                             39s   3GB
Jan 16 04:51:44 Starting compiler/backend/arm7/proofs
Jan 16 04:52:25 Finished compiler/backend/arm7/proofs                            40s   2GB
Jan 16 04:52:26 Starting compiler/backend/arm8/proofs
Jan 16 04:53:06 Finished compiler/backend/arm8/proofs                            38s   3GB
Jan 16 04:53:07 Starting compiler/backend/arm8_asl
Jan 16 04:53:34 Finished compiler/backend/arm8_asl                               26s   2GB
Jan 16 04:53:35 Starting compiler/backend/mips/proofs
Jan 16 04:54:18 Finished compiler/backend/mips/proofs                            42s   3GB
Jan 16 04:54:19 Starting compiler/backend/riscv/proofs
Jan 16 04:55:09 Finished compiler/backend/riscv/proofs                           49s   3GB
Jan 16 04:55:10 Starting compiler/backend/ag32/proofs
Jan 16 05:08:25 Finished compiler/backend/ag32/proofs                         13m15s   5GB
Jan 16 05:08:26 Starting candle/set-theory
Jan 16 05:09:10 Finished candle/set-theory                                       42s   1GB
Jan 16 05:09:11 Starting candle/syntax-lib
Jan 16 05:09:12 Finished candle/syntax-lib                                        0s  68MB
Jan 16 05:09:13 Starting candle/standard/syntax
Jan 16 05:09:29 Finished candle/standard/syntax                                  15s   1GB
Jan 16 05:09:30 Starting candle/standard/semantics
Jan 16 05:11:50 Finished candle/standard/semantics                             2m19s   2GB
Jan 16 05:11:51 Starting candle/standard/monadic
Jan 16 05:11:53 Finished candle/standard/monadic                                  0s 104MB
Jan 16 05:11:53 Starting candle/standard/ml_kernel
Jan 16 05:13:43 Finished candle/standard/ml_kernel                             1m49s   5GB
Jan 16 05:13:44 Starting candle/overloading/syntax
Jan 16 05:17:08 Finished candle/overloading/syntax                             3m23s   2GB
Jan 16 05:17:09 Starting candle/overloading/semantics
Jan 16 05:28:24 Finished candle/overloading/semantics                         11m14s   5GB
Jan 16 05:28:25 Starting candle/overloading/monadic
Jan 16 05:31:01 Finished candle/overloading/monadic                            2m34s   3GB
Jan 16 05:31:02 Starting candle/overloading/ml_kernel
Jan 16 05:38:32 Finished candle/overloading/ml_kernel                          7m29s   6GB
Jan 16 05:38:33 Starting candle/overloading/ml_checker
Jan 16 05:41:05 Finished candle/overloading/ml_checker                         2m31s   7GB
Jan 16 05:41:06 Starting candle/prover
Jan 16 05:50:59 Finished candle/prover                                         9m51s   5GB
Jan 16 05:51:00 Starting pancake
Jan 16 05:52:01 Finished pancake                                               1m00s   1GB
Jan 16 05:52:02 Starting pancake/ffi
Jan 16 05:52:03 Finished pancake/ffi                                              0s  19MB
Jan 16 05:52:04 Starting pancake/semantics
Jan 16 05:54:22 Finished pancake/semantics                                     2m17s   2GB
Jan 16 05:54:23 Starting pancake/parser
Jan 16 05:54:50 Finished pancake/parser                                          25s   1GB
Jan 16 05:54:50 Starting pancake/proofs
Jan 16 06:24:39 Finished pancake/proofs                                       29m48s   8GB
Jan 16 06:24:40 Starting characteristic/examples
Jan 16 06:26:18 Finished characteristic/examples                               1m36s   5GB
Jan 16 06:26:19 Starting tutorial/solutions
Jan 16 06:42:01 Finished tutorial/solutions                                   15m41s  12GB
Jan 16 06:42:02 Starting translator/monadic/examples
Jan 16 06:45:47 Finished translator/monadic/examples                           3m43s   4GB
Jan 16 06:45:48 Starting examples
Jan 16 07:00:23 Finished examples                                             14m34s   7GB
Jan 16 07:00:24 Starting examples/compilation/x64
Jan 16 08:58:07 Finished examples/compilation/x64                           1h57m41s  34GB
Jan 16 08:58:08 Starting examples/compilation/x64/proofs
Jan 16 09:01:57 Finished examples/compilation/x64/proofs                       3m47s   6GB
Jan 16 09:01:58 Starting examples/compilation/ag32
Jan 16 09:32:41 Finished examples/compilation/ag32                            30m42s  17GB
Jan 16 09:32:42 Starting examples/compilation/ag32/proofs
Jan 16 09:34:09 Finished examples/compilation/ag32/proofs                      1m26s   6GB
Jan 16 09:34:10 Starting examples/compilation/to_word
Jan 16 09:37:58 Finished examples/compilation/to_word                          3m46s  11GB
Jan 16 09:37:59 Starting examples/lpr_checker
Jan 16 09:39:13 Finished examples/lpr_checker                                  1m12s   2GB
Jan 16 09:39:13 Starting examples/lpr_checker/array
Jan 16 10:07:52 Finished examples/lpr_checker/array                           28m37s  10GB
Jan 16 10:07:53 Starting examples/lpr_checker/array/compilation
Jan 16 10:42:51 Finished examples/lpr_checker/array/compilation               34m57s  53GB
Jan 16 10:42:52 Starting examples/lpr_checker/array/compilation/proofs
Jan 16 10:44:47 Finished examples/lpr_checker/array/compilation/proofs         1m53s   9GB
Jan 16 10:44:47 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 16 11:07:29 Finished examples/lpr_checker/array/compilation/proofsARM8    22m40s  37GB
Jan 16 11:07:30 Starting examples/pseudo_bool
Jan 16 11:09:25 Finished examples/pseudo_bool                                  1m54s   1GB
Jan 16 11:09:26 Starting examples/pseudo_bool/cnf_encoding
Jan 16 11:10:00 Finished examples/pseudo_bool/cnf_encoding                       32s   1GB
Jan 16 11:10:01 Starting examples/pseudo_bool/graph_encoding
Jan 16 11:10:50 Finished examples/pseudo_bool/graph_encoding                     48s   2GB
Jan 16 11:10:51 Starting examples/pseudo_bool/array
Jan 16 12:00:31 Finished examples/pseudo_bool/array                           49m39s  16GB
Jan 16 12:00:32 Starting examples/pseudo_bool/array/compilation
Jan 16 13:49:30 Finished examples/pseudo_bool/array/compilation             1h48m57s  96GB
Jan 16 13:49:31 Starting examples/pseudo_bool/array/compilation/proofs
Jan 16 13:52:35 Finished examples/pseudo_bool/array/compilation/proofs         3m02s   7GB
Jan 16 13:52:36 Starting examples/opentheory
Jan 16 14:03:09 Finished examples/opentheory                                  10m32s   7GB
Jan 16 14:03:10 Starting examples/opentheory
Jan 16 14:03:12 Finished examples/opentheory                                      0s 123MB
Jan 16 14:03:13 Starting examples/opentheory/compilation
Jan 16 14:39:02 Finished examples/opentheory/compilation                      35m48s  53GB
Jan 16 14:39:03 Starting examples/opentheory/compilation/proofs
Jan 16 14:40:32 Finished examples/opentheory/compilation/proofs                1m28s   6GB
Jan 16 14:40:33 Starting examples/opentheory/compilation/ag32
Jan 16 15:12:10 Finished examples/opentheory/compilation/ag32                 31m36s  47GB
Jan 16 15:12:11 Starting examples/opentheory/compilation/ag32/proofs
Jan 16 15:14:29 Finished examples/opentheory/compilation/ag32/proofs           2m16s  11GB
Jan 16 15:14:29 Starting examples/sat_encodings
Jan 16 15:17:04 Finished examples/sat_encodings                                2m33s   1GB
Jan 16 15:17:05 Starting examples/sat_encodings/case_studies
Jan 16 15:19:03 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Jan 16 15:19:04 Starting examples/sat_encodings/translation
Jan 16 15:25:09 Finished examples/sat_encodings/translation                    6m04s   7GB
Jan 16 15:25:10 Starting examples/sat_encodings/translation/compilation
Jan 16 16:00:09 Finished examples/sat_encodings/translation/compilation       34m58s  37GB
Jan 16 16:00:10 Starting examples/deflate
Jan 16 16:01:23 Finished examples/deflate                                      1m11s   1GB
Jan 16 16:01:24 Starting examples/deflate/translation
Jan 16 16:02:59 Finished examples/deflate/translation                          1m34s   7GB
Jan 16 16:03:00 Starting examples/deflate/translation/compilation
Jan 16 16:19:10 Finished examples/deflate/translation/compilation             16m09s  21GB
Jan 16 16:19:11 Starting examples/vipr
Jan 16 16:23:18 Finished examples/vipr                                         4m05s   7GB
Jan 16 16:23:19 Starting examples/vipr/compilation
Jan 16 16:43:08 Finished examples/vipr/compilation                            19m48s  35GB
Jan 16 16:43:09 Starting translator/okasaki-examples
Jan 16 16:48:05 Finished translator/okasaki-examples                           4m55s   4GB
Jan 16 16:48:06 Starting translator/other-examples
Jan 16 16:51:42 Finished translator/other-examples                             3m34s   3GB
Jan 16 16:51:43 Starting compiler/parsing/tests
Jan 16 16:52:16 Finished compiler/parsing/tests                                  32s   1GB
Jan 16 16:52:17 Starting compiler/inference/tests
Jan 16 16:59:46 Finished compiler/inference/tests                              7m27s   7GB
Jan 16 16:59:47 Starting compiler/printing/test
Jan 16 17:03:16 Finished compiler/printing/test                                3m28s   6GB
Jan 16 17:03:17 Starting icing/flover
Jan 16 17:38:49 Finished icing/flover                                         35m30s   4GB
Jan 16 17:38:50 Starting icing/
Jan 16 18:33:28 Finished icing/                                               54m37s  31GB
Jan 16 18:33:29 Starting icing/examples
Jan 16 18:35:03 Finished icing/examples                                        1m32s   5GB
Jan 16 18:35:04 Starting compiler/repl
Jan 16 18:43:44 Finished compiler/repl                                         8m39s   9GB
Jan 16 18:43:45 Starting unverified/sexpr-bootstrap/x64/64
Jan 16 18:55:03 Finished unverified/sexpr-bootstrap/x64/64                    10m54s  15GB
Jan 16 18:55:03 Starting unverified/sexpr-bootstrap/x64/32
Jan 16 19:04:14 Finished unverified/sexpr-bootstrap/x64/32                     8m52s  14GB
Jan 16 19:04:14 Starting compiler/benchmarks
Jan 16 19:04:59 Finished compiler/benchmarks                                     43s 713MB
Jan 16 19:05:00 Starting compiler/bootstrap/compilation/x64/64
Jan 17 09:29:04 Finished compiler/bootstrap/compilation/x64/64             14h23m51s 153GB
Jan 17 09:29:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 17 09:50:16 Finished compiler/bootstrap/compilation/x64/64/proofs         21m11s  36GB
Jan 17 09:50:17 Starting compiler/bootstrap/compilation/x64/32
Jan 17 17:24:56 Finished compiler/bootstrap/compilation/x64/32              7h34m31s 136GB
Jan 17 17:24:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 17 17:28:38 Finished compiler/bootstrap/compilation/x64/32/proofs          3m40s  17GB
Jan 17 17:28:39 Starting compiler/bootstrap/compilation/ag32/32
Jan 18 01:16:10 Finished compiler/bootstrap/compilation/ag32/32             7h47m29s 147GB
Jan 18 01:16:11 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 18 01:24:01 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m48s  48GB
Jan 18 01:24:02 SUCCESS