Job 2023

CakeML:2d85a9fbcf10fb4eb1398f75958ce621218d4c19
  Fix alt_semantics missing a case [Oct 14 07:57:09]
#911 (libm_gen)
Merging into:8f0d65ee6ef75967a24c98e0efcaef83606cbafe
  Fix some breakage [Oct 26 12:53:15]
HOL:d0be848293e4de8a9b3179ad479e5ee5e184cb35
  Minor update to documentation of splitting fields. [Oct 19 02:06:16]
Machine:oven3

Oct 26 12:58:21 Claimed job
Oct 26 12:58:26 Reusing HOL
Oct 26 12:59:20 Starting developers
Oct 26 12:59:29 Finished developers                                               9s 108MB
Oct 26 12:59:30 Starting developers/bin
Oct 26 12:59:44 Finished developers/bin                                          13s   1GB
Oct 26 12:59:44 Starting compiler/proofs
Oct 26 16:21:19 Finished compiler/proofs                                    3h21m34s  16GB
Oct 26 16:21:19 Starting compiler/bootstrap/translation
Oct 27 02:46:49 Finished compiler/bootstrap/translation                    10h25m29s  39GB
Oct 27 02:46:50 Starting semantics/ffi
Oct 27 02:46:57 Finished semantics/ffi                                            7s 214MB
Oct 27 02:46:57 Starting semantics
Oct 27 02:47:00 Finished semantics                                                2s  17MB
Oct 27 02:47:00 Starting semantics/proofs
Oct 27 02:48:09 Finished semantics/proofs                                      1m08s 612MB
Oct 27 02:48:09 Starting semantics/alt_semantics
Oct 27 02:49:06 Finished semantics/alt_semantics                                 56s 648MB
Oct 27 02:49:06 Starting semantics/alt_semantics/proofs
Oct 27 03:15:17 Finished semantics/alt_semantics/proofs                       26m10s   1GB
Oct 27 03:15:17 Starting basis/pure
Oct 27 03:15:20 Finished basis/pure                                               2s  33MB
Oct 27 03:15:20 Starting translator
Oct 27 03:19:03 Finished translator                                            3m42s   1GB
Oct 27 03:19:03 Starting compiler/parsing
Oct 27 03:19:06 Finished compiler/parsing                                         2s  33MB
Oct 27 03:19:06 Starting characteristic
Oct 27 03:19:10 Finished characteristic                                           3s  25MB
Oct 27 03:19:10 Starting translator/monadic
Oct 27 03:19:13 Finished translator/monadic                                       2s  33MB
Oct 27 03:19:13 Starting basis
Oct 27 03:26:38 Finished basis                                                 7m24s   2GB
Oct 27 03:26:38 Starting compiler/inference
Oct 27 03:26:41 Finished compiler/inference                                       2s  26MB
Oct 27 03:26:41 Starting compiler/backend/reg_alloc
Oct 27 03:26:44 Finished compiler/backend/reg_alloc                               2s  17MB
Oct 27 03:26:44 Starting compiler/backend/gc
Oct 27 03:26:48 Finished compiler/backend/gc                                      3s  26MB
Oct 27 03:26:48 Starting compiler/backend
Oct 27 03:27:12 Finished compiler/backend                                        23s 669MB
Oct 27 03:27:13 Starting compiler/encoders/asm
Oct 27 03:27:16 Finished compiler/encoders/asm                                    2s  23MB
Oct 27 03:27:16 Starting compiler/encoders/x64
Oct 27 03:27:19 Finished compiler/encoders/x64                                    2s  34MB
Oct 27 03:27:19 Starting compiler/encoders/arm7
Oct 27 03:27:22 Finished compiler/encoders/arm7                                   2s  34MB
Oct 27 03:27:22 Starting compiler/encoders/arm8
Oct 27 03:27:25 Finished compiler/encoders/arm8                                   2s  32MB
Oct 27 03:27:25 Starting compiler/encoders/arm8_asl
Oct 27 07:39:43 Finished compiler/encoders/arm8_asl                         4h12m17s  25GB
Oct 27 07:39:44 Starting compiler/encoders/mips
Oct 27 07:39:47 Finished compiler/encoders/mips                                   2s  24MB
Oct 27 07:39:47 Starting compiler/encoders/riscv
Oct 27 07:39:50 Finished compiler/encoders/riscv                                  2s  29MB
Oct 27 07:39:50 Starting compiler/encoders/ag32
Oct 27 07:39:53 Finished compiler/encoders/ag32                                   2s  27MB
Oct 27 07:39:53 Starting compiler/backend/x64
Oct 27 07:39:57 Finished compiler/backend/x64                                     3s  33MB
Oct 27 07:39:57 Starting compiler/backend/arm7
Oct 27 07:40:01 Finished compiler/backend/arm7                                    3s  33MB
Oct 27 07:40:01 Starting compiler/backend/arm8
Oct 27 07:40:05 Finished compiler/backend/arm8                                    3s  33MB
Oct 27 07:40:05 Starting compiler/backend/mips
Oct 27 07:40:09 Finished compiler/backend/mips                                    3s  28MB
Oct 27 07:40:09 Starting compiler/backend/riscv
Oct 27 07:40:13 Finished compiler/backend/riscv                                   3s  26MB
Oct 27 07:40:13 Starting compiler/backend/ag32
Oct 27 07:43:06 Finished compiler/backend/ag32                                 2m52s   1GB
Oct 27 07:43:06 Starting compiler/parsing/proofs
Oct 27 07:43:09 Finished compiler/parsing/proofs                                  2s  30MB
Oct 27 07:43:09 Starting compiler/inference/proofs
Oct 27 07:43:12 Finished compiler/inference/proofs                                2s  25MB
Oct 27 07:43:13 Starting compiler/backend/semantics
Oct 27 07:45:34 Finished compiler/backend/semantics                            2m20s   1GB
Oct 27 07:45:34 Starting compiler/backend/reg_alloc/proofs
Oct 27 07:45:38 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Oct 27 07:45:38 Starting compiler/backend/proofs
Oct 27 07:47:40 Finished compiler/backend/proofs                               2m02s   2GB
Oct 27 07:47:41 Starting compiler/backend/serialiser
Oct 27 07:47:46 Finished compiler/backend/serialiser                              5s  49MB
Oct 27 07:47:46 Starting compiler/encoders/x64/proofs
Oct 27 08:09:34 Finished compiler/encoders/x64/proofs                         21m47s   5GB
Oct 27 08:09:34 Starting compiler/encoders/arm7/proofs
Oct 27 08:40:17 Finished compiler/encoders/arm7/proofs                        30m42s   5GB
Oct 27 08:40:17 Starting compiler/encoders/arm8/proofs
Oct 27 08:56:10 Finished compiler/encoders/arm8/proofs                        15m52s   1GB
Oct 27 08:56:10 Starting compiler/encoders/arm8_asl/proofs
Oct 27 10:49:45 Finished compiler/encoders/arm8_asl/proofs                  1h53m34s   6GB
Oct 27 10:49:45 Starting compiler/encoders/mips/proofs
Oct 27 11:13:00 Finished compiler/encoders/mips/proofs                        23m14s   3GB
Oct 27 11:13:00 Starting compiler/encoders/riscv/proofs
Oct 27 11:33:21 Finished compiler/encoders/riscv/proofs                       20m20s   1GB
Oct 27 11:33:22 Starting compiler/encoders/ag32/proofs
Oct 27 11:39:14 Finished compiler/encoders/ag32/proofs                         5m51s   1GB
Oct 27 11:39:14 Starting compiler/backend/x64/proofs
Oct 27 11:40:06 Finished compiler/backend/x64/proofs                             52s   1GB
Oct 27 11:40:06 Starting compiler/backend/arm7/proofs
Oct 27 11:41:05 Finished compiler/backend/arm7/proofs                            57s   1GB
Oct 27 11:41:05 Starting compiler/backend/arm8/proofs
Oct 27 11:42:02 Finished compiler/backend/arm8/proofs                            56s   1GB
Oct 27 11:42:02 Starting compiler/backend/arm8_asl
Oct 27 11:42:46 Finished compiler/backend/arm8_asl                               43s   1GB
Oct 27 11:42:46 Starting compiler/backend/mips/proofs
Oct 27 11:43:39 Finished compiler/backend/mips/proofs                            52s   1GB
Oct 27 11:43:39 Starting compiler/backend/riscv/proofs
Oct 27 11:44:32 Finished compiler/backend/riscv/proofs                           52s   1GB
Oct 27 11:44:32 Starting compiler/backend/ag32/proofs
Oct 27 12:14:00 Finished compiler/backend/ag32/proofs                         29m27s   3GB
Oct 27 12:14:00 Starting candle/set-theory
Oct 27 12:15:09 Finished candle/set-theory                                     1m08s   1GB
Oct 27 12:15:09 Starting candle/syntax-lib
Oct 27 12:15:12 Finished candle/syntax-lib                                        2s  33MB
Oct 27 12:15:12 Starting candle/standard/syntax
Oct 27 12:15:32 Finished candle/standard/syntax                                  19s 531MB
Oct 27 12:15:32 Starting candle/standard/semantics
Oct 27 12:19:24 Finished candle/standard/semantics                             3m51s   1GB
Oct 27 12:19:25 Starting candle/standard/monadic
Oct 27 12:19:28 Finished candle/standard/monadic                                  3s  33MB
Oct 27 12:19:28 Starting candle/standard/ml_kernel
Oct 27 12:22:27 Finished candle/standard/ml_kernel                             2m58s   2GB
Oct 27 12:22:28 Starting candle/overloading/syntax
Oct 27 12:29:20 Finished candle/overloading/syntax                             6m52s   1GB
Oct 27 12:29:21 Starting candle/overloading/semantics
Oct 27 12:56:04 Finished candle/overloading/semantics                         26m42s   2GB
Oct 27 12:56:04 Starting candle/overloading/monadic
Oct 27 13:01:36 Finished candle/overloading/monadic                            5m31s   1GB
Oct 27 13:01:36 Starting candle/overloading/ml_kernel
Oct 27 13:17:13 Finished candle/overloading/ml_kernel                         15m36s   3GB
Oct 27 13:17:13 Starting candle/overloading/ml_checker
Oct 27 13:22:36 Finished candle/overloading/ml_checker                         5m22s   3GB
Oct 27 13:22:36 Starting candle/prover
Oct 27 13:37:07 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(240s)     OK
Starting work on compute_evalProofTheory
candle_kernel_permsTheory                                                                                                                                                              candle/prover(433s)     OK
compute_evalProofTheory                                                                                                                                                        candle/prover/compute(189s)     OK
Starting work on compute_execProofTheory
compute_execProofTheory                                                                                                                                                        candle/prover/compute (28s)     OK
Starting work on computeProofTheory
computeProofTheory                                                                                                                                                             candle/prover/compute(112s)     OK
Finished $(CAKEMLDIR)/candle/prover/compute [#theories: 4]                                                                                                                                             (570.845s) 
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                                                                                                                                               candle/prover(174s)     OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory                                                                                                                                                           candle/prover (96s)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"}