Job 2033

CakeML:2d85a9fbcf10fb4eb1398f75958ce621218d4c19
  Fix alt_semantics missing a case [Oct 14 07:57:09]
#911 (libm_gen)
Merging into:3d27e77937edd037e810801a4e7849352300104f
  Add [schematic] to a definition (suggested by @mn200) [Nov 07 20:36:24]
HOL:126d898e2a2195a717f5757375b93570965286f1
  Cleanup and tweak release notes for next version in a few places [Nov 03 06:41:06]
Machine:oven3

Nov 07 20:44:51 Claimed job
Nov 07 20:44:53 Reusing HOL
Nov 07 20:45:47 Starting developers
Nov 07 20:45:56 Finished developers                                               9s  84MB
Nov 07 20:45:56 Starting developers/bin
Nov 07 20:46:09 Finished developers/bin                                          12s   1GB
Nov 07 20:46:09 Starting compiler/proofs
Nov 08 00:07:51 Finished compiler/proofs                                    3h21m41s  17GB
Nov 08 00:07:51 Starting compiler/bootstrap/translation
Nov 08 10:25:35 Finished compiler/bootstrap/translation                    10h17m43s  60GB
Nov 08 10:25:35 Starting semantics/ffi
Nov 08 10:25:42 Finished semantics/ffi                                            6s 222MB
Nov 08 10:25:43 Starting semantics
Nov 08 10:25:45 Finished semantics                                                2s  33MB
Nov 08 10:25:45 Starting semantics/proofs
Nov 08 10:26:52 Finished semantics/proofs                                      1m06s 806MB
Nov 08 10:26:53 Starting semantics/alt_semantics
Nov 08 10:27:51 Finished semantics/alt_semantics                                 58s 590MB
Nov 08 10:27:52 Starting semantics/alt_semantics/proofs
Nov 08 10:54:06 Finished semantics/alt_semantics/proofs                       26m14s   1GB
Nov 08 10:54:06 Starting basis/pure
Nov 08 10:54:09 Finished basis/pure                                               2s  33MB
Nov 08 10:54:09 Starting translator
Nov 08 10:57:55 Finished translator                                            3m45s   1GB
Nov 08 10:57:55 Starting compiler/parsing
Nov 08 10:57:57 Finished compiler/parsing                                         2s  33MB
Nov 08 10:57:58 Starting characteristic
Nov 08 10:58:01 Finished characteristic                                           3s  26MB
Nov 08 10:58:01 Starting translator/monadic
Nov 08 10:58:05 Finished translator/monadic                                       3s  43MB
Nov 08 10:58:05 Starting basis
Nov 08 11:05:40 Finished basis                                                 7m34s   2GB
Nov 08 11:05:40 Starting compiler/inference
Nov 08 11:05:43 Finished compiler/inference                                       2s  31MB
Nov 08 11:05:43 Starting compiler/backend/reg_alloc
Nov 08 11:05:45 Finished compiler/backend/reg_alloc                               2s  35MB
Nov 08 11:05:46 Starting compiler/backend/gc
Nov 08 11:05:49 Finished compiler/backend/gc                                      3s  33MB
Nov 08 11:05:49 Starting compiler/backend
Nov 08 11:06:13 Finished compiler/backend                                        23s 645MB
Nov 08 11:06:14 Starting compiler/encoders/asm
Nov 08 11:06:17 Finished compiler/encoders/asm                                    2s  25MB
Nov 08 11:06:17 Starting compiler/encoders/x64
Nov 08 11:06:20 Finished compiler/encoders/x64                                    2s  24MB
Nov 08 11:06:20 Starting compiler/encoders/arm7
Nov 08 11:06:23 Finished compiler/encoders/arm7                                   2s  25MB
Nov 08 11:06:23 Starting compiler/encoders/arm8
Nov 08 11:06:26 Finished compiler/encoders/arm8                                   2s  26MB
Nov 08 11:06:27 Starting compiler/encoders/arm8_asl
Nov 08 15:27:12 Finished compiler/encoders/arm8_asl                         4h20m45s  40GB
Nov 08 15:27:12 Starting compiler/encoders/mips
Nov 08 15:27:15 Finished compiler/encoders/mips                                   2s  36MB
Nov 08 15:27:16 Starting compiler/encoders/riscv
Nov 08 15:27:19 Finished compiler/encoders/riscv                                  2s  35MB
Nov 08 15:27:19 Starting compiler/encoders/ag32
Nov 08 15:27:22 Finished compiler/encoders/ag32                                   2s  21MB
Nov 08 15:27:22 Starting compiler/backend/x64
Nov 08 15:27:26 Finished compiler/backend/x64                                     3s  26MB
Nov 08 15:27:26 Starting compiler/backend/arm7
Nov 08 15:27:30 Finished compiler/backend/arm7                                    3s  32MB
Nov 08 15:27:30 Starting compiler/backend/arm8
Nov 08 15:27:34 Finished compiler/backend/arm8                                    3s  32MB
Nov 08 15:27:35 Starting compiler/backend/mips
Nov 08 15:27:38 Finished compiler/backend/mips                                    3s  35MB
Nov 08 15:27:38 Starting compiler/backend/riscv
Nov 08 15:27:42 Finished compiler/backend/riscv                                   3s  35MB
Nov 08 15:27:43 Starting compiler/backend/ag32
Nov 08 15:30:40 Finished compiler/backend/ag32                                 2m57s   1GB
Nov 08 15:30:41 Starting compiler/parsing/proofs
Nov 08 15:30:44 Finished compiler/parsing/proofs                                  2s  33MB
Nov 08 15:30:44 Starting compiler/inference/proofs
Nov 08 15:30:47 Finished compiler/inference/proofs                                2s  27MB
Nov 08 15:30:47 Starting compiler/backend/semantics
Nov 08 15:33:10 Finished compiler/backend/semantics                            2m22s   1GB
Nov 08 15:33:11 Starting compiler/backend/reg_alloc/proofs
Nov 08 15:33:14 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Nov 08 15:33:14 Starting compiler/backend/proofs
Nov 08 15:35:06 Finished compiler/backend/proofs                               1m51s   2GB
Nov 08 15:35:06 Starting compiler/backend/serialiser
Nov 08 15:35:11 Finished compiler/backend/serialiser                              4s  28MB
Nov 08 15:35:11 Starting compiler/encoders/x64/proofs
Nov 08 15:57:26 Finished compiler/encoders/x64/proofs                         22m14s   4GB
Nov 08 15:57:26 Starting compiler/encoders/arm7/proofs
Nov 08 16:27:58 Finished compiler/encoders/arm7/proofs                        30m31s   3GB
Nov 08 16:27:59 Starting compiler/encoders/arm8/proofs
Nov 08 16:43:45 Finished compiler/encoders/arm8/proofs                        15m46s   1GB
Nov 08 16:43:45 Starting compiler/encoders/arm8_asl/proofs
Nov 08 18:38:36 Finished compiler/encoders/arm8_asl/proofs                  1h54m49s   6GB
Nov 08 18:38:36 Starting compiler/encoders/mips/proofs
Nov 08 19:02:42 Finished compiler/encoders/mips/proofs                        24m05s   2GB
Nov 08 19:02:42 Starting compiler/encoders/riscv/proofs
Nov 08 19:22:57 Finished compiler/encoders/riscv/proofs                       20m14s   1GB
Nov 08 19:22:58 Starting compiler/encoders/ag32/proofs
Nov 08 19:28:55 Finished compiler/encoders/ag32/proofs                         5m57s 839MB
Nov 08 19:28:55 Starting compiler/backend/x64/proofs
Nov 08 19:29:49 Finished compiler/backend/x64/proofs                             53s   1GB
Nov 08 19:29:50 Starting compiler/backend/arm7/proofs
Nov 08 19:30:44 Finished compiler/backend/arm7/proofs                            54s   1GB
Nov 08 19:30:44 Starting compiler/backend/arm8/proofs
Nov 08 19:31:41 Finished compiler/backend/arm8/proofs                            55s   1GB
Nov 08 19:31:41 Starting compiler/backend/arm8_asl
Nov 08 19:32:25 Finished compiler/backend/arm8_asl                               43s   1GB
Nov 08 19:32:25 Starting compiler/backend/mips/proofs
Nov 08 19:33:21 Finished compiler/backend/mips/proofs                            55s   1GB
Nov 08 19:33:22 Starting compiler/backend/riscv/proofs
Nov 08 19:34:18 Finished compiler/backend/riscv/proofs                           56s   1GB
Nov 08 19:34:19 Starting compiler/backend/ag32/proofs
Nov 08 20:05:00 Finished compiler/backend/ag32/proofs                         30m40s   2GB
Nov 08 20:05:00 Starting candle/set-theory
Nov 08 20:06:07 Finished candle/set-theory                                     1m07s   1GB
Nov 08 20:06:08 Starting candle/syntax-lib
Nov 08 20:06:10 Finished candle/syntax-lib                                        2s  17MB
Nov 08 20:06:10 Starting candle/standard/syntax
Nov 08 20:06:31 Finished candle/standard/syntax                                  19s 531MB
Nov 08 20:06:31 Starting candle/standard/semantics
Nov 08 20:10:28 Finished candle/standard/semantics                             3m56s   1GB
Nov 08 20:10:28 Starting candle/standard/monadic
Nov 08 20:10:31 Finished candle/standard/monadic                                  2s  37MB
Nov 08 20:10:31 Starting candle/standard/ml_kernel
Nov 08 20:13:34 Finished candle/standard/ml_kernel                             3m02s   3GB
Nov 08 20:13:34 Starting candle/overloading/syntax
Nov 08 20:20:35 Finished candle/overloading/syntax                             7m00s   1GB
Nov 08 20:20:35 Starting candle/overloading/semantics
Nov 08 20:47:02 Finished candle/overloading/semantics                         26m25s   2GB
Nov 08 20:47:02 Starting candle/overloading/monadic
Nov 08 20:52:35 Finished candle/overloading/monadic                            5m32s   2GB
Nov 08 20:52:35 Starting candle/overloading/ml_kernel
Nov 08 21:07:59 Finished candle/overloading/ml_kernel                         15m23s   4GB
Nov 08 21:07:59 Starting candle/overloading/ml_checker
Nov 08 21:13:23 Finished candle/overloading/ml_checker                         5m23s   3GB
Nov 08 21:13:23 Starting candle/prover
Nov 08 21:28:22 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(248s)     OK
Starting work on compute_evalProofTheory
candle_kernel_permsTheory                                                                                                                                                              candle/prover(393s)     OK
compute_evalProofTheory                                                                                                                                                        candle/prover/compute(199s)     OK
Starting work on compute_execProofTheory
compute_execProofTheory                                                                                                                                                        candle/prover/compute (28s)     OK
Starting work on computeProofTheory
computeProofTheory                                                                                                                                                             candle/prover/compute(113s)     OK
Finished $(CAKEMLDIR)/candle/prover/compute [#theories: 4]                                                                                                                                             (589.827s) 
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                                                                                                                                               candle/prover(169s)     OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory                                                                                                                                                           candle/prover(110s)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"}