Job 2156

CakeML:ca3e595e8ff524933b16be2b8004025b16afb935
  Fix a Theorem-Proof-QED error now flagged by most recent HOL [Jun 21 01:34:16]
HOL:643c7c5191f649af6f9c0b347660ad62d9617dc2
  Fix ASL equivalence proofs [Jun 18 03:48:18]
Machine:pavlova

Jun 21 01:44:16 Claimed job
Jun 21 01:44:20 Reusing HOL
Jun 21 01:44:30 Starting developers
Jun 21 01:44:33 Finished developers                                               2s 182MB
Jun 21 01:44:34 Starting developers/bin
Jun 21 01:44:44 Finished developers/bin                                           9s   1GB
Jun 21 01:44:45 Starting compiler/proofs
Jun 21 03:25:10 Finished compiler/proofs                                    1h40m23s  34GB
Jun 21 03:25:11 Starting compiler/bootstrap/translation
Jun 21 11:24:18 Finished compiler/bootstrap/translation                     7h59m06s  60GB
Jun 21 11:24:19 Starting semantics/ffi
Jun 21 11:24:27 Finished semantics/ffi                                            7s 614MB
Jun 21 11:24:27 Starting semantics
Jun 21 11:24:29 Finished semantics                                                0s  63MB
Jun 21 11:24:29 Starting semantics/proofs
Jun 21 11:25:05 Finished semantics/proofs                                        35s   2GB
Jun 21 11:25:06 Starting semantics/alt_semantics
Jun 21 11:25:46 Finished semantics/alt_semantics                                 38s   1GB
Jun 21 11:25:47 Starting semantics/alt_semantics/proofs
Jun 21 11:36:53 Finished semantics/alt_semantics/proofs                       11m05s   3GB
Jun 21 11:36:54 Starting basis/pure
Jun 21 11:36:55 Finished basis/pure                                               0s  72MB
Jun 21 11:36:56 Starting translator
Jun 21 11:38:38 Finished translator                                            1m41s   4GB
Jun 21 11:38:39 Starting compiler/parsing
Jun 21 11:38:40 Finished compiler/parsing                                         0s  70MB
Jun 21 11:38:41 Starting characteristic
Jun 21 11:38:43 Finished characteristic                                           0s  93MB
Jun 21 11:38:44 Starting translator/monadic
Jun 21 11:38:45 Finished translator/monadic                                       0s  90MB
Jun 21 11:38:46 Starting basis
Jun 21 11:42:35 Finished basis                                                 3m48s   5GB
Jun 21 11:42:36 Starting compiler/inference
Jun 21 11:42:37 Finished compiler/inference                                       0s  82MB
Jun 21 11:42:38 Starting compiler/backend/reg_alloc
Jun 21 11:42:39 Finished compiler/backend/reg_alloc                               0s  67MB
Jun 21 11:42:40 Starting compiler/backend/gc
Jun 21 11:42:42 Finished compiler/backend/gc                                      0s 137MB
Jun 21 11:42:43 Starting compiler/backend
Jun 21 11:43:00 Finished compiler/backend                                        16s   1GB
Jun 21 11:43:01 Starting compiler/encoders/asm
Jun 21 11:43:02 Finished compiler/encoders/asm                                    0s  89MB
Jun 21 11:43:03 Starting compiler/encoders/x64
Jun 21 11:43:05 Finished compiler/encoders/x64                                    0s  90MB
Jun 21 11:43:06 Starting compiler/encoders/arm7
Jun 21 11:43:07 Finished compiler/encoders/arm7                                   0s  90MB
Jun 21 11:43:08 Starting compiler/encoders/arm8
Jun 21 11:43:09 Finished compiler/encoders/arm8                                   0s  90MB
Jun 21 11:43:10 Starting compiler/encoders/arm8_asl
Jun 21 11:45:22 Finished compiler/encoders/arm8_asl                            2m10s   1GB
Jun 21 11:45:23 Starting compiler/encoders/mips
Jun 21 11:45:24 Finished compiler/encoders/mips                                   0s  90MB
Jun 21 11:45:25 Starting compiler/encoders/riscv
Jun 21 11:45:26 Finished compiler/encoders/riscv                                  0s  89MB
Jun 21 11:45:27 Starting compiler/encoders/ag32
Jun 21 11:45:28 Finished compiler/encoders/ag32                                   0s  89MB
Jun 21 11:45:29 Starting compiler/backend/x64
Jun 21 11:45:31 Finished compiler/backend/x64                                     0s 129MB
Jun 21 11:45:32 Starting compiler/backend/arm7
Jun 21 11:45:34 Finished compiler/backend/arm7                                    0s 129MB
Jun 21 11:45:34 Starting compiler/backend/arm8
Jun 21 11:45:36 Finished compiler/backend/arm8                                    0s 123MB
Jun 21 11:45:37 Starting compiler/backend/mips
Jun 21 11:45:39 Finished compiler/backend/mips                                    0s 129MB
Jun 21 11:45:39 Starting compiler/backend/riscv
Jun 21 11:45:41 Finished compiler/backend/riscv                                   0s 129MB
Jun 21 11:45:42 Starting compiler/backend/ag32
Jun 21 11:47:07 Finished compiler/backend/ag32                                 1m23s   3GB
Jun 21 11:47:08 Starting compiler/parsing/proofs
Jun 21 11:47:09 Finished compiler/parsing/proofs                                  0s  72MB
Jun 21 11:47:10 Starting compiler/inference/proofs
Jun 21 11:47:11 Finished compiler/inference/proofs                                0s  88MB
Jun 21 11:47:12 Starting compiler/backend/semantics
Jun 21 11:48:36 Finished compiler/backend/semantics                            1m23s   2GB
Jun 21 11:48:37 Starting compiler/backend/reg_alloc/proofs
Jun 21 11:48:39 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Jun 21 11:48:40 Starting compiler/backend/proofs
Jun 21 11:49:42 Finished compiler/backend/proofs                               1m01s   3GB
Jun 21 11:49:42 Starting compiler/backend/serialiser
Jun 21 11:49:45 Finished compiler/backend/serialiser                              1s 180MB
Jun 21 11:49:45 Starting compiler/encoders/x64/proofs
Jun 21 11:59:08 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Jun 21 11:59:09 Starting compiler/encoders/arm7/proofs
Jun 21 12:12:17 Finished compiler/encoders/arm7/proofs                        13m06s   8GB
Jun 21 12:12:18 Starting compiler/encoders/arm8/proofs
Jun 21 12:18:47 Finished compiler/encoders/arm8/proofs                         6m28s   4GB
Jun 21 12:18:48 Starting compiler/encoders/arm8_asl/proofs
Jun 21 12:32:59 Finished compiler/encoders/arm8_asl/proofs                    14m09s   4GB
Jun 21 12:33:00 Starting compiler/encoders/mips/proofs
Jun 21 12:43:12 Finished compiler/encoders/mips/proofs                        10m10s   5GB
Jun 21 12:43:13 Starting compiler/encoders/riscv/proofs
Jun 21 12:51:36 Finished compiler/encoders/riscv/proofs                        8m22s   3GB
Jun 21 12:51:36 Starting compiler/encoders/ag32/proofs
Jun 21 12:54:02 Finished compiler/encoders/ag32/proofs                         2m24s   2GB
Jun 21 12:54:03 Starting compiler/backend/x64/proofs
Jun 21 12:54:43 Finished compiler/backend/x64/proofs                             39s   3GB
Jun 21 12:54:44 Starting compiler/backend/arm7/proofs
Jun 21 12:55:26 Finished compiler/backend/arm7/proofs                            41s   2GB
Jun 21 12:55:26 Starting compiler/backend/arm8/proofs
Jun 21 12:56:10 Finished compiler/backend/arm8/proofs                            42s   3GB
Jun 21 12:56:11 Starting compiler/backend/arm8_asl
Jun 21 12:56:39 Finished compiler/backend/arm8_asl                               27s   2GB
Jun 21 12:56:40 Starting compiler/backend/mips/proofs
Jun 21 12:57:23 Finished compiler/backend/mips/proofs                            42s   3GB
Jun 21 12:57:24 Starting compiler/backend/riscv/proofs
Jun 21 12:58:11 Finished compiler/backend/riscv/proofs                           46s   3GB
Jun 21 12:58:12 Starting compiler/backend/ag32/proofs
Jun 21 13:11:40 Finished compiler/backend/ag32/proofs                         13m26s   6GB
Jun 21 13:11:41 Starting candle/set-theory
Jun 21 13:12:26 Finished candle/set-theory                                       44s   1GB
Jun 21 13:12:27 Starting candle/syntax-lib
Jun 21 13:12:28 Finished candle/syntax-lib                                        0s  70MB
Jun 21 13:12:29 Starting candle/standard/syntax
Jun 21 13:12:46 Finished candle/standard/syntax                                  16s   1GB
Jun 21 13:12:47 Starting candle/standard/semantics
Jun 21 13:15:13 Finished candle/standard/semantics                             2m25s   3GB
Jun 21 13:15:14 Starting candle/standard/monadic
Jun 21 13:15:16 Finished candle/standard/monadic                                  0s 105MB
Jun 21 13:15:17 Starting candle/standard/ml_kernel
Jun 21 13:17:04 Finished candle/standard/ml_kernel                             1m46s   4GB
Jun 21 13:17:04 Starting candle/overloading/syntax
Jun 21 13:20:31 Finished candle/overloading/syntax                             3m25s   3GB
Jun 21 13:20:32 Starting candle/overloading/semantics
Jun 21 13:31:47 Finished candle/overloading/semantics                         11m14s   6GB
Jun 21 13:31:48 Starting candle/overloading/monadic
Jun 21 13:34:25 Finished candle/overloading/monadic                            2m34s   3GB
Jun 21 13:34:25 Starting candle/overloading/ml_kernel
Jun 21 13:41:59 Finished candle/overloading/ml_kernel                          7m32s   7GB
Jun 21 13:42:00 Starting candle/overloading/ml_checker
Jun 21 13:44:33 Finished candle/overloading/ml_checker                         2m32s   7GB
Jun 21 13:44:34 Starting candle/prover
Jun 21 13:54:37 Finished candle/prover                                        10m02s   4GB
Jun 21 13:54:38 Starting pancake
Jun 21 13:55:38 Finished pancake                                                 59s   1GB
Jun 21 13:55:39 Starting pancake/ffi
Jun 21 13:55:40 Finished pancake/ffi                                              0s  21MB
Jun 21 13:55:41 Starting pancake/semantics
Jun 21 13:57:59 Finished pancake/semantics                                     2m17s   3GB
Jun 21 13:58:00 Starting pancake/proofs
Jun 21 14:15:07 Finished pancake/proofs                                       17m06s   5GB
Jun 21 14:15:08 Starting characteristic/examples
Jun 21 14:16:41 Finished characteristic/examples                               1m31s   5GB
Jun 21 14:16:42 Starting tutorial/solutions
Jun 21 14:31:46 Finished tutorial/solutions                                   15m03s  10GB
Jun 21 14:31:47 Starting translator/monadic/examples
Jun 21 14:35:27 Finished translator/monadic/examples                           3m39s   4GB
Jun 21 14:35:28 Starting examples
Jun 21 14:50:07 Finished examples                                             14m37s   7GB
Jun 21 14:50:07 Starting examples/compilation/x64
Jun 21 16:44:58 Finished examples/compilation/x64                           1h54m48s  17GB
Jun 21 16:44:59 Starting examples/compilation/x64/proofs
Jun 21 16:48:42 Finished examples/compilation/x64/proofs                       3m42s   6GB
Jun 21 16:48:43 Starting examples/compilation/ag32
Jun 21 17:18:46 Finished examples/compilation/ag32                            30m02s   9GB
Jun 21 17:18:47 Starting examples/compilation/ag32/proofs
Jun 21 17:20:13 Finished examples/compilation/ag32/proofs                      1m25s   7GB
Jun 21 17:20:14 Starting examples/compilation/to_word
Jun 21 17:24:09 Finished examples/compilation/to_word                          3m54s  10GB
Jun 21 17:24:10 Starting examples/lpr_checker
Jun 21 17:25:15 FAILED: examples/lpr_checker
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanned 29 directories
Starting work on README.md
Starting work on satSemTheory
README.md                                                           (0s)     OK
satSemTheory                                                       (17s)     OK
Starting work on lprTheory
lprTheory                                                          (22s)     OK
Starting work on lpr_parsingTheory
Starting work on packingTheory
Starting work on ramseyTheory
lpr_parsingTheory                                                  (17s)FAIL<1>
 Saved theorem _______ "max_lit_max_1"
 Saved theorem _______ "max_lit_max"
 Saved theorem _______ "max_lit_max_lit_max"
 Saved theorem _______ "parse_dimacs_body_length"
 Saved theorem _______ "parse_dimacs_toks_print_dimacs_toks"
 Saved theorem _______ "parse_dimacs_print_dimacs"
 /scratch/cakeml/regression/cakeml-2156/examples/lpr_checker/lpr_parsingScript.sml:495: error: ; expected but ) was found
 error in quse /scratch/cakeml/regression/cakeml-2156/examples/lpr_checker/lpr_parsingScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-2156/examples/lpr_checker/lpr_parsingScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
packingTheory                                                      (17s)MKILLED
ramseyTheory                                                       (17s)MKILLED