Job 2027

CakeML:2d85a9fbcf10fb4eb1398f75958ce621218d4c19
  Fix alt_semantics missing a case [Oct 14 07:57:09]
#911 (libm_gen)
Merging into:1c3099821c836fea2d95e30c03368d0cb6838441
  Merge pull request #914 from CakeML/lpr_parse [Oct 28 11:58:21]
HOL:4c12fddb3f1c114611290a420d3a1ac4a32a44d8
  Update some of relationScript.sml to modern style [Oct 26 03:25:37]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Oct 30 11:14:58 Claimed job
Oct 30 11:15:00 Reusing HOL
Oct 30 11:15:40 Starting developers
Oct 30 11:15:45 Finished developers                                               5s  92MB
Oct 30 11:15:45 Starting developers/bin
Oct 30 11:15:51 Finished developers/bin                                           5s   1GB
Oct 30 11:15:52 Starting compiler/proofs
Oct 30 13:00:03 Finished compiler/proofs                                    1h44m09s  15GB
Oct 30 13:00:03 Starting compiler/bootstrap/translation
Oct 30 17:49:49 Finished compiler/bootstrap/translation                     4h49m43s  45GB
Oct 30 17:49:49 Starting semantics/ffi
Oct 30 17:49:54 Finished semantics/ffi                                            4s 142MB
Oct 30 17:49:54 Starting semantics
Oct 30 17:49:56 Finished semantics                                                1s  19MB
Oct 30 17:49:56 Starting semantics/proofs
Oct 30 17:50:27 Finished semantics/proofs                                        30s 853MB
Oct 30 17:50:27 Starting semantics/alt_semantics
Oct 30 17:50:55 Finished semantics/alt_semantics                                 28s 529MB
Oct 30 17:50:55 Starting semantics/alt_semantics/proofs
Oct 30 18:02:44 Finished semantics/alt_semantics/proofs                       11m48s   1GB
Oct 30 18:02:44 Starting basis/pure
Oct 30 18:02:46 Finished basis/pure                                               1s  21MB
Oct 30 18:02:46 Starting translator
Oct 30 18:04:34 Finished translator                                            1m48s   1GB
Oct 30 18:04:35 Starting compiler/parsing
Oct 30 18:04:36 Finished compiler/parsing                                         1s  18MB
Oct 30 18:04:36 Starting characteristic
Oct 30 18:04:38 Finished characteristic                                           1s  25MB
Oct 30 18:04:38 Starting translator/monadic
Oct 30 18:04:40 Finished translator/monadic                                       1s  30MB
Oct 30 18:04:40 Starting basis
Oct 30 18:08:05 Finished basis                                                 3m24s   2GB
Oct 30 18:08:05 Starting compiler/inference
Oct 30 18:08:07 Finished compiler/inference                                       1s  23MB
Oct 30 18:08:07 Starting compiler/backend/reg_alloc
Oct 30 18:08:09 Finished compiler/backend/reg_alloc                               1s  19MB
Oct 30 18:08:09 Starting compiler/backend/gc
Oct 30 18:08:11 Finished compiler/backend/gc                                      2s  34MB
Oct 30 18:08:11 Starting compiler/backend
Oct 30 18:08:22 Finished compiler/backend                                        10s 554MB
Oct 30 18:08:22 Starting compiler/encoders/asm
Oct 30 18:08:24 Finished compiler/encoders/asm                                    1s  19MB
Oct 30 18:08:24 Starting compiler/encoders/x64
Oct 30 18:08:25 Finished compiler/encoders/x64                                    1s  22MB
Oct 30 18:08:26 Starting compiler/encoders/arm7
Oct 30 18:08:27 Finished compiler/encoders/arm7                                   1s  20MB
Oct 30 18:08:28 Starting compiler/encoders/arm8
Oct 30 18:08:29 Finished compiler/encoders/arm8                                   1s  35MB
Oct 30 18:08:29 Starting compiler/encoders/arm8_asl
Oct 30 18:11:39 Finished compiler/encoders/arm8_asl                            3m09s   1GB
Oct 30 18:11:39 Starting compiler/encoders/mips
Oct 30 18:11:41 Finished compiler/encoders/mips                                   1s  23MB
Oct 30 18:11:41 Starting compiler/encoders/riscv
Oct 30 18:11:43 Finished compiler/encoders/riscv                                  1s  19MB
Oct 30 18:11:43 Starting compiler/encoders/ag32
Oct 30 18:11:44 Finished compiler/encoders/ag32                                   1s  23MB
Oct 30 18:11:45 Starting compiler/backend/x64
Oct 30 18:11:47 Finished compiler/backend/x64                                     2s  35MB
Oct 30 18:11:47 Starting compiler/backend/arm7
Oct 30 18:11:49 Finished compiler/backend/arm7                                    2s  34MB
Oct 30 18:11:49 Starting compiler/backend/arm8
Oct 30 18:11:51 Finished compiler/backend/arm8                                    2s  29MB
Oct 30 18:11:52 Starting compiler/backend/mips
Oct 30 18:11:54 Finished compiler/backend/mips                                    2s  23MB
Oct 30 18:11:54 Starting compiler/backend/riscv
Oct 30 18:11:56 Finished compiler/backend/riscv                                   2s  33MB
Oct 30 18:11:56 Starting compiler/backend/ag32
Oct 30 18:13:23 Finished compiler/backend/ag32                                 1m26s   1GB
Oct 30 18:13:24 Starting compiler/parsing/proofs
Oct 30 18:13:25 Finished compiler/parsing/proofs                                  1s  19MB
Oct 30 18:13:25 Starting compiler/inference/proofs
Oct 30 18:13:27 Finished compiler/inference/proofs                                1s  34MB
Oct 30 18:13:27 Starting compiler/backend/semantics
Oct 30 18:14:34 Finished compiler/backend/semantics                            1m06s   1GB
Oct 30 18:14:34 Starting compiler/backend/reg_alloc/proofs
Oct 30 18:14:36 Finished compiler/backend/reg_alloc/proofs                        1s  34MB
Oct 30 18:14:36 Starting compiler/backend/proofs
Oct 30 18:15:30 Finished compiler/backend/proofs                                 53s   2GB
Oct 30 18:15:30 Starting compiler/backend/serialiser
Oct 30 18:15:33 Finished compiler/backend/serialiser                              2s  41MB
Oct 30 18:15:33 Starting compiler/encoders/x64/proofs
Oct 30 18:25:16 Finished compiler/encoders/x64/proofs                          9m42s   5GB
Oct 30 18:25:16 Starting compiler/encoders/arm7/proofs
Oct 30 18:38:58 Finished compiler/encoders/arm7/proofs                        13m42s   3GB
Oct 30 18:38:59 Starting compiler/encoders/arm8/proofs
Oct 30 18:45:55 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Oct 30 18:45:55 Starting compiler/encoders/arm8_asl/proofs
Oct 30 19:02:02 Finished compiler/encoders/arm8_asl/proofs                    16m05s   2GB
Oct 30 19:02:02 Starting compiler/encoders/mips/proofs
Oct 30 19:12:28 Finished compiler/encoders/mips/proofs                        10m25s   3GB
Oct 30 19:12:28 Starting compiler/encoders/riscv/proofs
Oct 30 19:21:36 Finished compiler/encoders/riscv/proofs                        9m07s   1GB
Oct 30 19:21:36 Starting compiler/encoders/ag32/proofs
Oct 30 19:24:14 Finished compiler/encoders/ag32/proofs                         2m37s 837MB
Oct 30 19:24:15 Starting compiler/backend/x64/proofs
Oct 30 19:24:41 Finished compiler/backend/x64/proofs                             26s   1GB
Oct 30 19:24:41 Starting compiler/backend/arm7/proofs
Oct 30 19:25:08 Finished compiler/backend/arm7/proofs                            27s   1GB
Oct 30 19:25:08 Starting compiler/backend/arm8/proofs
Oct 30 19:25:36 Finished compiler/backend/arm8/proofs                            27s   1GB
Oct 30 19:25:37 Starting compiler/backend/arm8_asl
Oct 30 19:25:57 Finished compiler/backend/arm8_asl                               20s   1GB
Oct 30 19:25:58 Starting compiler/backend/mips/proofs
Oct 30 19:26:24 Finished compiler/backend/mips/proofs                            26s   1GB
Oct 30 19:26:24 Starting compiler/backend/riscv/proofs
Oct 30 19:26:51 Finished compiler/backend/riscv/proofs                           26s   1GB
Oct 30 19:26:52 Starting compiler/backend/ag32/proofs
Oct 30 19:40:41 Finished compiler/backend/ag32/proofs                         13m49s   2GB
Oct 30 19:40:41 Starting candle/set-theory
Oct 30 19:41:17 Finished candle/set-theory                                       35s 998MB
Oct 30 19:41:17 Starting candle/syntax-lib
Oct 30 19:41:19 Finished candle/syntax-lib                                        1s  20MB
Oct 30 19:41:19 Starting candle/standard/syntax
Oct 30 19:41:28 Finished candle/standard/syntax                                   8s 550MB
Oct 30 19:41:28 Starting candle/standard/semantics
Oct 30 19:43:13 Finished candle/standard/semantics                             1m44s   1GB
Oct 30 19:43:13 Starting candle/standard/monadic
Oct 30 19:43:15 Finished candle/standard/monadic                                  1s  35MB
Oct 30 19:43:15 Starting candle/standard/ml_kernel
Oct 30 19:44:42 Finished candle/standard/ml_kernel                             1m27s   2GB
Oct 30 19:44:43 Starting candle/overloading/syntax
Oct 30 19:47:56 Finished candle/overloading/syntax                             3m13s   1GB
Oct 30 19:47:56 Starting candle/overloading/semantics
Oct 30 19:59:51 Finished candle/overloading/semantics                         11m55s   2GB
Oct 30 19:59:52 Starting candle/overloading/monadic
Oct 30 20:02:29 Finished candle/overloading/monadic                            2m36s   1GB
Oct 30 20:02:29 Starting candle/overloading/ml_kernel
Oct 30 20:10:01 Finished candle/overloading/ml_kernel                          7m31s   3GB
Oct 30 20:10:01 Starting candle/overloading/ml_checker
Oct 30 20:12:26 Finished candle/overloading/ml_checker                         2m25s   3GB
Oct 30 20:12:26 Starting candle/prover
Oct 30 20:19:00 FAILED: candle/prover
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
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover/compute[0m
Scanned 37 directories
Starting work on compute_syntaxProofTheory
Starting work on README.md
Starting work on candle_kernel_permsTheory
README.md                                                                                                                                                        candle/prover  (0s)     OK
compute_syntaxProofTheory                                                                                                                                candle/prover/compute(105s)     OK
Starting work on compute_evalProofTheory
candle_kernel_permsTheory                                                                                                                                        candle/prover(181s)     OK
compute_evalProofTheory                                                                                                                                  candle/prover/compute (87s)     OK
Starting work on compute_execProofTheory
compute_execProofTheory                                                                                                                                  candle/prover/compute (12s)     OK
Starting work on computeProofTheory
computeProofTheory                                                                                                                                       candle/prover/compute (47s)     OK
Finished $(CAKEMLDIR)/candle/prover/compute [#theories: 4]                                                                                                                       (253.846s) 
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                                                                                                                         candle/prover (83s)     OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory                                                                                                                                     candle/prover (43s)FAIL<1>
   STATE ctxt st1  (loc. loc  kernel_locs  kernel_loc_ok st1 loc refs1) 
   (loc r. loc  kernel_locs  LLOOKUP refs1 loc = SOME r  ref_ok ctxt r) 
   EVERY ok_event ffi1.io_events 
   case list_result res of
     Rval vs => EVERY (v_ok ctxt) vs
   | Rerr (Rraise v) => v_ok ctxt v
   | Rerr (Rabort v8) => T
 
 Failed to prove theorem do_app_ok.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}