Job 2157

CakeML:754414b1e27a33ce3c216e4544a3f83ba9d82d62
  Fix another parse error in Theorem-Proof syntax [Jun 21 22:42:54]
HOL:643c7c5191f649af6f9c0b347660ad62d9617dc2
  Fix ASL equivalence proofs [Jun 18 03:48:18]
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

Jun 21 22:45:40 Claimed job
Jun 21 22:45:45 Reusing HOL
Jun 21 22:45:54 Starting developers
Jun 21 22:45:58 Finished developers                                               2s 205MB
Jun 21 22:45:58 Starting developers/bin
Jun 21 22:46:08 Finished developers/bin                                           9s   1GB
Jun 21 22:46:09 Starting compiler/proofs
Jun 22 00:27:41 Finished compiler/proofs                                    1h41m30s  30GB
Jun 22 00:27:42 Starting compiler/bootstrap/translation
Jun 22 08:28:09 Finished compiler/bootstrap/translation                     8h00m25s  77GB
Jun 22 08:28:09 Starting semantics/ffi
Jun 22 08:28:17 Finished semantics/ffi                                            7s 613MB
Jun 22 08:28:18 Starting semantics
Jun 22 08:28:19 Finished semantics                                                0s  64MB
Jun 22 08:28:20 Starting semantics/proofs
Jun 22 08:28:56 Finished semantics/proofs                                        34s   2GB
Jun 22 08:28:57 Starting semantics/alt_semantics
Jun 22 08:29:38 Finished semantics/alt_semantics                                 40s   1GB
Jun 22 08:29:38 Starting semantics/alt_semantics/proofs
Jun 22 08:40:36 Finished semantics/alt_semantics/proofs                       10m57s   5GB
Jun 22 08:40:37 Starting basis/pure
Jun 22 08:40:38 Finished basis/pure                                               0s  68MB
Jun 22 08:40:39 Starting translator
Jun 22 08:42:23 Finished translator                                            1m42s   4GB
Jun 22 08:42:24 Starting compiler/parsing
Jun 22 08:42:25 Finished compiler/parsing                                         0s  70MB
Jun 22 08:42:26 Starting characteristic
Jun 22 08:42:28 Finished characteristic                                           0s  92MB
Jun 22 08:42:28 Starting translator/monadic
Jun 22 08:42:30 Finished translator/monadic                                       0s  95MB
Jun 22 08:42:31 Starting basis
Jun 22 08:46:22 Finished basis                                                 3m50s   5GB
Jun 22 08:46:23 Starting compiler/inference
Jun 22 08:46:24 Finished compiler/inference                                       0s  81MB
Jun 22 08:46:25 Starting compiler/backend/reg_alloc
Jun 22 08:46:26 Finished compiler/backend/reg_alloc                               0s  67MB
Jun 22 08:46:27 Starting compiler/backend/gc
Jun 22 08:46:29 Finished compiler/backend/gc                                      0s 129MB
Jun 22 08:46:30 Starting compiler/backend
Jun 22 08:46:47 Finished compiler/backend                                        16s   1GB
Jun 22 08:46:48 Starting compiler/encoders/asm
Jun 22 08:46:49 Finished compiler/encoders/asm                                    0s  89MB
Jun 22 08:46:50 Starting compiler/encoders/x64
Jun 22 08:46:52 Finished compiler/encoders/x64                                    0s  90MB
Jun 22 08:46:52 Starting compiler/encoders/arm7
Jun 22 08:46:54 Finished compiler/encoders/arm7                                   0s  90MB
Jun 22 08:46:55 Starting compiler/encoders/arm8
Jun 22 08:46:56 Finished compiler/encoders/arm8                                   0s  90MB
Jun 22 08:46:57 Starting compiler/encoders/arm8_asl
Jun 22 08:49:06 Finished compiler/encoders/arm8_asl                            2m08s   1GB
Jun 22 08:49:07 Starting compiler/encoders/mips
Jun 22 08:49:09 Finished compiler/encoders/mips                                   0s  90MB
Jun 22 08:49:10 Starting compiler/encoders/riscv
Jun 22 08:49:11 Finished compiler/encoders/riscv                                  0s  89MB
Jun 22 08:49:12 Starting compiler/encoders/ag32
Jun 22 08:49:13 Finished compiler/encoders/ag32                                   0s  89MB
Jun 22 08:49:14 Starting compiler/backend/x64
Jun 22 08:49:16 Finished compiler/backend/x64                                     0s 134MB
Jun 22 08:49:17 Starting compiler/backend/arm7
Jun 22 08:49:18 Finished compiler/backend/arm7                                    0s 128MB
Jun 22 08:49:19 Starting compiler/backend/arm8
Jun 22 08:49:21 Finished compiler/backend/arm8                                    0s 128MB
Jun 22 08:49:22 Starting compiler/backend/mips
Jun 22 08:49:23 Finished compiler/backend/mips                                    0s 128MB
Jun 22 08:49:24 Starting compiler/backend/riscv
Jun 22 08:49:26 Finished compiler/backend/riscv                                   0s 128MB
Jun 22 08:49:27 Starting compiler/backend/ag32
Jun 22 08:50:48 Finished compiler/backend/ag32                                 1m19s   2GB
Jun 22 08:50:48 Starting compiler/parsing/proofs
Jun 22 08:50:50 Finished compiler/parsing/proofs                                  0s  72MB
Jun 22 08:50:51 Starting compiler/inference/proofs
Jun 22 08:50:52 Finished compiler/inference/proofs                                0s  88MB
Jun 22 08:50:53 Starting compiler/backend/semantics
Jun 22 08:52:18 Finished compiler/backend/semantics                            1m24s   2GB
Jun 22 08:52:19 Starting compiler/backend/reg_alloc/proofs
Jun 22 08:52:21 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Jun 22 08:52:22 Starting compiler/backend/proofs
Jun 22 08:53:23 Finished compiler/backend/proofs                               1m00s   2GB
Jun 22 08:53:24 Starting compiler/backend/serialiser
Jun 22 08:53:26 Finished compiler/backend/serialiser                              1s 193MB
Jun 22 08:53:27 Starting compiler/encoders/x64/proofs
Jun 22 09:02:57 Finished compiler/encoders/x64/proofs                          9m28s   5GB
Jun 22 09:02:58 Starting compiler/encoders/arm7/proofs
Jun 22 09:16:07 Finished compiler/encoders/arm7/proofs                        13m08s  12GB
Jun 22 09:16:08 Starting compiler/encoders/arm8/proofs
Jun 22 09:22:37 Finished compiler/encoders/arm8/proofs                         6m27s   6GB
Jun 22 09:22:37 Starting compiler/encoders/arm8_asl/proofs
Jun 22 09:36:29 Finished compiler/encoders/arm8_asl/proofs                    13m49s   4GB
Jun 22 09:36:30 Starting compiler/encoders/mips/proofs
Jun 22 09:46:39 Finished compiler/encoders/mips/proofs                        10m07s   6GB
Jun 22 09:46:39 Starting compiler/encoders/riscv/proofs
Jun 22 09:54:51 Finished compiler/encoders/riscv/proofs                        8m10s   3GB
Jun 22 09:54:52 Starting compiler/encoders/ag32/proofs
Jun 22 09:57:18 Finished compiler/encoders/ag32/proofs                         2m25s   2GB
Jun 22 09:57:19 Starting compiler/backend/x64/proofs
Jun 22 09:57:59 Finished compiler/backend/x64/proofs                             38s   3GB
Jun 22 09:57:59 Starting compiler/backend/arm7/proofs
Jun 22 09:58:47 Finished compiler/backend/arm7/proofs                            47s   3GB
Jun 22 09:58:48 Starting compiler/backend/arm8/proofs
Jun 22 09:59:28 Finished compiler/backend/arm8/proofs                            38s   3GB
Jun 22 09:59:29 Starting compiler/backend/arm8_asl
Jun 22 09:59:58 Finished compiler/backend/arm8_asl                               28s   2GB
Jun 22 09:59:59 Starting compiler/backend/mips/proofs
Jun 22 10:00:43 Finished compiler/backend/mips/proofs                            42s   3GB
Jun 22 10:00:44 Starting compiler/backend/riscv/proofs
Jun 22 10:01:31 Finished compiler/backend/riscv/proofs                           47s   3GB
Jun 22 10:01:32 Starting compiler/backend/ag32/proofs
Jun 22 10:14:50 Finished compiler/backend/ag32/proofs                         13m16s   5GB
Jun 22 10:14:51 Starting candle/set-theory
Jun 22 10:15:36 Finished candle/set-theory                                       44s   1GB
Jun 22 10:15:37 Starting candle/syntax-lib
Jun 22 10:15:38 Finished candle/syntax-lib                                        0s  73MB
Jun 22 10:15:39 Starting candle/standard/syntax
Jun 22 10:15:55 Finished candle/standard/syntax                                  15s   1GB
Jun 22 10:15:56 Starting candle/standard/semantics
Jun 22 10:18:20 Finished candle/standard/semantics                             2m23s   3GB
Jun 22 10:18:21 Starting candle/standard/monadic
Jun 22 10:18:23 Finished candle/standard/monadic                                  0s 105MB
Jun 22 10:18:23 Starting candle/standard/ml_kernel
Jun 22 10:20:16 Finished candle/standard/ml_kernel                             1m51s   6GB
Jun 22 10:20:17 Starting candle/overloading/syntax
Jun 22 10:23:44 Finished candle/overloading/syntax                             3m26s   3GB
Jun 22 10:23:45 Starting candle/overloading/semantics
Jun 22 10:35:20 Finished candle/overloading/semantics                         11m34s   4GB
Jun 22 10:35:21 Starting candle/overloading/monadic
Jun 22 10:37:54 Finished candle/overloading/monadic                            2m31s   2GB
Jun 22 10:37:55 Starting candle/overloading/ml_kernel
Jun 22 10:45:26 Finished candle/overloading/ml_kernel                          7m29s   6GB
Jun 22 10:45:26 Starting candle/overloading/ml_checker
Jun 22 10:47:56 Finished candle/overloading/ml_checker                         2m28s   7GB
Jun 22 10:47:57 Starting candle/prover
Jun 22 10:57:47 Finished candle/prover                                         9m48s   5GB
Jun 22 10:57:48 Starting pancake
Jun 22 10:58:48 Finished pancake                                                 59s   1GB
Jun 22 10:58:48 Starting pancake/ffi
Jun 22 10:58:49 Finished pancake/ffi                                              0s  19MB
Jun 22 10:58:50 Starting pancake/semantics
Jun 22 11:01:09 Finished pancake/semantics                                     2m18s   2GB
Jun 22 11:01:10 Starting pancake/proofs
Jun 22 11:18:30 Finished pancake/proofs                                       17m19s   6GB
Jun 22 11:18:31 Starting characteristic/examples
Jun 22 11:20:05 Finished characteristic/examples                               1m33s   6GB
Jun 22 11:20:06 Starting tutorial/solutions
Jun 22 11:35:27 Finished tutorial/solutions                                   15m19s  15GB
Jun 22 11:35:27 Starting translator/monadic/examples
Jun 22 11:39:09 Finished translator/monadic/examples                           3m40s   5GB
Jun 22 11:39:09 Starting examples
Jun 22 11:53:29 Finished examples                                             14m18s   7GB
Jun 22 11:53:30 Starting examples/compilation/x64
Jun 22 13:48:34 Finished examples/compilation/x64                           1h55m02s  19GB
Jun 22 13:48:34 Starting examples/compilation/x64/proofs
Jun 22 13:52:17 Finished examples/compilation/x64/proofs                       3m41s   6GB
Jun 22 13:52:18 Starting examples/compilation/ag32
Jun 22 14:22:36 Finished examples/compilation/ag32                            30m17s   9GB
Jun 22 14:22:37 Starting examples/compilation/ag32/proofs
Jun 22 14:24:05 Finished examples/compilation/ag32/proofs                      1m27s   6GB
Jun 22 14:24:06 Starting examples/compilation/to_word
Jun 22 14:27:56 Finished examples/compilation/to_word                          3m49s  11GB
Jun 22 14:27:56 Starting examples/lpr_checker
Jun 22 14:29:10 Finished examples/lpr_checker                                  1m12s   2GB
Jun 22 14:29:11 Starting examples/lpr_checker/array
Jun 22 15:04:07 Finished examples/lpr_checker/array                           34m54s  10GB
Jun 22 15:04:08 Starting examples/lpr_checker/array/compilation
Jun 22 15:39:28 Finished examples/lpr_checker/array/compilation               35m19s  58GB
Jun 22 15:39:29 Starting examples/lpr_checker/array/compilation/proofs
Jun 22 15:41:19 Finished examples/lpr_checker/array/compilation/proofs         1m49s   9GB
Jun 22 15:41:20 Starting examples/opentheory
Jun 22 15:52:10 Finished examples/opentheory                                  10m49s   7GB
Jun 22 15:52:11 Starting examples/opentheory
Jun 22 15:52:13 Finished examples/opentheory                                      0s 128MB
Jun 22 15:52:14 Starting examples/opentheory/compilation
Jun 22 16:27:58 Finished examples/opentheory/compilation                      35m42s  52GB
Jun 22 16:27:59 Starting examples/opentheory/compilation/proofs
Jun 22 16:29:25 Finished examples/opentheory/compilation/proofs                1m25s   6GB
Jun 22 16:29:26 Starting examples/opentheory/compilation/ag32
Jun 22 17:01:36 Finished examples/opentheory/compilation/ag32                 32m09s  71GB
Jun 22 17:01:37 Starting examples/opentheory/compilation/ag32/proofs
Jun 22 17:03:54 Finished examples/opentheory/compilation/ag32/proofs           2m15s  11GB
Jun 22 17:03:55 Starting examples/sat_encodings
Jun 22 17:06:30 Finished examples/sat_encodings                                2m34s   1GB
Jun 22 17:06:31 Starting examples/sat_encodings/case_studies
Jun 22 17:08:31 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Jun 22 17:08:32 Starting examples/sat_encodings/translation
Jun 22 17:14:34 Finished examples/sat_encodings/translation                    6m01s   7GB
Jun 22 17:14:35 Starting examples/sat_encodings/translation/compilation
Jun 22 17:48:52 Finished examples/sat_encodings/translation/compilation       34m14s  44GB
Jun 22 17:48:53 Starting examples/deflate
Jun 22 17:50:09 Finished examples/deflate                                      1m14s   1GB
Jun 22 17:50:10 Starting examples/deflate/translation
Jun 22 17:51:46 Finished examples/deflate/translation                          1m34s   7GB
Jun 22 17:51:46 Starting examples/deflate/translation/compilation
Jun 22 18:07:41 Finished examples/deflate/translation/compilation             15m53s  17GB
Jun 22 18:07:42 Starting examples/vipr
Jun 22 18:11:39 Finished examples/vipr                                         3m56s   7GB
Jun 22 18:11:40 Starting examples/vipr/compilation
Jun 22 18:31:17 Finished examples/vipr/compilation                            19m36s  17GB
Jun 22 18:31:17 Starting translator/okasaki-examples
Jun 22 18:36:25 Finished translator/okasaki-examples                           5m06s   3GB
Jun 22 18:36:26 Starting translator/other-examples
Jun 22 18:40:07 Finished translator/other-examples                             3m40s   3GB
Jun 22 18:40:08 Starting compiler/parsing/tests
Jun 22 18:40:42 Finished compiler/parsing/tests                                  33s   1GB
Jun 22 18:40:43 Starting compiler/inference/tests
Jun 22 18:48:17 Finished compiler/inference/tests                              7m33s   6GB
Jun 22 18:48:17 Starting compiler/printing/test
Jun 22 18:51:56 Finished compiler/printing/test                                3m36s   6GB
Jun 22 18:51:57 Starting icing/flover
Jun 22 19:27:40 Finished icing/flover                                         35m42s   3GB
Jun 22 19:27:41 Starting icing/
Jun 22 20:23:47 Finished icing/                                               56m04s  33GB
Jun 22 20:23:48 Starting icing/examples
Jun 22 20:25:29 Finished icing/examples                                        1m40s   8GB
Jun 22 20:25:30 Starting compiler/repl
Jun 22 20:34:21 Finished compiler/repl                                         8m50s   8GB
Jun 22 20:34:22 Starting unverified/sexpr-bootstrap/x64/64
Jun 22 20:45:40 Finished unverified/sexpr-bootstrap/x64/64                    10m56s  15GB
Jun 22 20:45:41 Starting unverified/sexpr-bootstrap/x64/32
Jun 22 20:55:08 Finished unverified/sexpr-bootstrap/x64/32                     8m57s  13GB
Jun 22 20:55:09 Starting compiler/benchmarks
Jun 22 20:55:54 Finished compiler/benchmarks                                     43s 713MB
Jun 22 20:55:54 Starting compiler/bootstrap/compilation/x64/64
Jun 23 10:44:46 Finished compiler/bootstrap/compilation/x64/64             13h48m30s 143GB
Jun 23 10:44:46 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 23 11:06:06 Finished compiler/bootstrap/compilation/x64/64/proofs         21m18s  44GB
Jun 23 11:06:06 Starting compiler/bootstrap/compilation/x64/32
Jun 23 18:03:30 Finished compiler/bootstrap/compilation/x64/32              6h57m16s 113GB
Jun 23 18:03:30 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 23 18:07:08 Finished compiler/bootstrap/compilation/x64/32/proofs          3m36s  19GB
Jun 23 18:07:09 Starting compiler/bootstrap/compilation/ag32/32
Jun 24 01:10:44 Finished compiler/bootstrap/compilation/ag32/32             7h03m32s 135GB
Jun 24 01:10:44 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 24 01:18:10 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m25s  48GB
Jun 24 01:18:11 SUCCESS