Job 2028

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:ccf43ef36fec1370be70f86eb2e927901d170f49
  Mention the Armv8 memory model port in the release notes [Nov 02 05:47:15]
Machine:oven3

Nov 03 18:37:22 Claimed job
Nov 03 18:37:32 Building HOL
Nov 03 19:00:28 Starting developers
Nov 03 19:00:38 Finished developers                                               9s  98MB
Nov 03 19:00:38 Starting developers/bin
Nov 03 19:00:51 Finished developers/bin                                          12s   1GB
Nov 03 19:00:52 Starting compiler/proofs
Nov 03 22:31:06 Finished compiler/proofs                                    3h30m13s  16GB
Nov 03 22:31:06 Starting compiler/bootstrap/translation
Nov 04 08:53:39 Finished compiler/bootstrap/translation                    10h22m32s  42GB
Nov 04 08:53:40 Starting semantics/ffi
Nov 04 08:53:47 Finished semantics/ffi                                            7s 193MB
Nov 04 08:53:48 Starting semantics
Nov 04 08:53:50 Finished semantics                                                2s  32MB
Nov 04 08:53:50 Starting semantics/proofs
Nov 04 08:55:02 Finished semantics/proofs                                      1m11s 612MB
Nov 04 08:55:03 Starting semantics/alt_semantics
Nov 04 08:55:59 Finished semantics/alt_semantics                                 55s 528MB
Nov 04 08:55:59 Starting semantics/alt_semantics/proofs
Nov 04 09:22:18 Finished semantics/alt_semantics/proofs                       26m18s   1GB
Nov 04 09:22:18 Starting basis/pure
Nov 04 09:22:20 Finished basis/pure                                               2s  32MB
Nov 04 09:22:21 Starting translator
Nov 04 09:26:02 Finished translator                                            3m41s   1GB
Nov 04 09:26:03 Starting compiler/parsing
Nov 04 09:26:05 Finished compiler/parsing                                         2s  24MB
Nov 04 09:26:05 Starting characteristic
Nov 04 09:26:09 Finished characteristic                                           3s  25MB
Nov 04 09:26:09 Starting translator/monadic
Nov 04 09:26:12 Finished translator/monadic                                       2s  32MB
Nov 04 09:26:12 Starting basis
Nov 04 09:33:40 Finished basis                                                 7m26s   3GB
Nov 04 09:33:40 Starting compiler/inference
Nov 04 09:33:43 Finished compiler/inference                                       2s  22MB
Nov 04 09:33:43 Starting compiler/backend/reg_alloc
Nov 04 09:33:46 Finished compiler/backend/reg_alloc                               2s  26MB
Nov 04 09:33:46 Starting compiler/backend/gc
Nov 04 09:33:50 Finished compiler/backend/gc                                      3s  37MB
Nov 04 09:33:50 Starting compiler/backend
Nov 04 09:34:15 Finished compiler/backend                                        25s 624MB
Nov 04 09:34:16 Starting compiler/encoders/asm
Nov 04 09:34:19 Finished compiler/encoders/asm                                    2s  23MB
Nov 04 09:34:19 Starting compiler/encoders/x64
Nov 04 09:34:22 Finished compiler/encoders/x64                                    2s  23MB
Nov 04 09:34:22 Starting compiler/encoders/arm7
Nov 04 09:34:25 Finished compiler/encoders/arm7                                   2s  27MB
Nov 04 09:34:25 Starting compiler/encoders/arm8
Nov 04 09:34:28 Finished compiler/encoders/arm8                                   2s  30MB
Nov 04 09:34:29 Starting compiler/encoders/arm8_asl
Nov 04 13:55:24 Finished compiler/encoders/arm8_asl                         4h20m55s  42GB
Nov 04 13:55:25 Starting compiler/encoders/mips
Nov 04 13:55:28 Finished compiler/encoders/mips                                   2s  33MB
Nov 04 13:55:28 Starting compiler/encoders/riscv
Nov 04 13:55:31 Finished compiler/encoders/riscv                                  2s  31MB
Nov 04 13:55:31 Starting compiler/encoders/ag32
Nov 04 13:55:34 Finished compiler/encoders/ag32                                   2s  26MB
Nov 04 13:55:34 Starting compiler/backend/x64
Nov 04 13:55:38 Finished compiler/backend/x64                                     3s  33MB
Nov 04 13:55:38 Starting compiler/backend/arm7
Nov 04 13:55:42 Finished compiler/backend/arm7                                    3s  33MB
Nov 04 13:55:42 Starting compiler/backend/arm8
Nov 04 13:55:46 Finished compiler/backend/arm8                                    3s  34MB
Nov 04 13:55:46 Starting compiler/backend/mips
Nov 04 13:55:50 Finished compiler/backend/mips                                    3s  32MB
Nov 04 13:55:50 Starting compiler/backend/riscv
Nov 04 13:55:54 Finished compiler/backend/riscv                                   3s  31MB
Nov 04 13:55:55 Starting compiler/backend/ag32
Nov 04 13:58:53 Finished compiler/backend/ag32                                 2m57s   1GB
Nov 04 13:58:53 Starting compiler/parsing/proofs
Nov 04 13:58:56 Finished compiler/parsing/proofs                                  2s  21MB
Nov 04 13:58:56 Starting compiler/inference/proofs
Nov 04 13:58:59 Finished compiler/inference/proofs                                2s  33MB
Nov 04 13:58:59 Starting compiler/backend/semantics
Nov 04 14:01:24 Finished compiler/backend/semantics                            2m24s   1GB
Nov 04 14:01:25 Starting compiler/backend/reg_alloc/proofs
Nov 04 14:01:28 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Nov 04 14:01:28 Starting compiler/backend/proofs
Nov 04 14:03:30 Finished compiler/backend/proofs                               2m01s   3GB
Nov 04 14:03:30 Starting compiler/backend/serialiser
Nov 04 14:03:35 Finished compiler/backend/serialiser                              4s  33MB
Nov 04 14:03:36 Starting compiler/encoders/x64/proofs
Nov 04 14:25:38 Finished compiler/encoders/x64/proofs                         22m01s   4GB
Nov 04 14:25:38 Starting compiler/encoders/arm7/proofs
Nov 04 14:56:28 Finished compiler/encoders/arm7/proofs                        30m49s   3GB
Nov 04 14:56:28 Starting compiler/encoders/arm8/proofs
Nov 04 15:12:33 Finished compiler/encoders/arm8/proofs                        16m04s   1GB
Nov 04 15:12:33 Starting compiler/encoders/arm8_asl/proofs
Nov 04 17:10:36 Finished compiler/encoders/arm8_asl/proofs                  1h58m02s   8GB
Nov 04 17:10:37 Starting compiler/encoders/mips/proofs
Nov 04 17:34:33 Finished compiler/encoders/mips/proofs                        23m56s   2GB
Nov 04 17:34:34 Starting compiler/encoders/riscv/proofs
Nov 04 17:54:58 Finished compiler/encoders/riscv/proofs                       20m24s   1GB
Nov 04 17:54:58 Starting compiler/encoders/ag32/proofs
Nov 04 18:00:50 Finished compiler/encoders/ag32/proofs                         5m51s 987MB
Nov 04 18:00:50 Starting compiler/backend/x64/proofs
Nov 04 18:01:42 Finished compiler/backend/x64/proofs                             52s   1GB
Nov 04 18:01:43 Starting compiler/backend/arm7/proofs
Nov 04 18:02:41 Finished compiler/backend/arm7/proofs                            58s   1GB
Nov 04 18:02:42 Starting compiler/backend/arm8/proofs
Nov 04 18:03:40 Finished compiler/backend/arm8/proofs                            58s   1GB
Nov 04 18:03:40 Starting compiler/backend/arm8_asl
Nov 04 18:04:27 Finished compiler/backend/arm8_asl                               45s   1GB
Nov 04 18:04:27 Starting compiler/backend/mips/proofs
Nov 04 18:05:21 Finished compiler/backend/mips/proofs                            53s   1GB
Nov 04 18:05:21 Starting compiler/backend/riscv/proofs
Nov 04 18:06:16 Finished compiler/backend/riscv/proofs                           54s   1GB
Nov 04 18:06:17 Starting compiler/backend/ag32/proofs
Nov 04 18:36:23 Finished compiler/backend/ag32/proofs                         30m06s   2GB
Nov 04 18:36:23 Starting candle/set-theory
Nov 04 18:37:32 Finished candle/set-theory                                     1m08s 977MB
Nov 04 18:37:32 Starting candle/syntax-lib
Nov 04 18:37:35 Finished candle/syntax-lib                                        2s  33MB
Nov 04 18:37:35 Starting candle/standard/syntax
Nov 04 18:37:55 Finished candle/standard/syntax                                  19s 534MB
Nov 04 18:37:55 Starting candle/standard/semantics
Nov 04 18:41:48 Finished candle/standard/semantics                             3m52s   1GB
Nov 04 18:41:48 Starting candle/standard/monadic
Nov 04 18:41:51 Finished candle/standard/monadic                                  2s  33MB
Nov 04 18:41:51 Starting candle/standard/ml_kernel
Nov 04 18:44:55 Finished candle/standard/ml_kernel                             3m04s   3GB
Nov 04 18:44:56 Starting candle/overloading/syntax
Nov 04 18:52:01 Finished candle/overloading/syntax                             7m05s   1GB
Nov 04 18:52:02 Starting candle/overloading/semantics
Nov 04 19:18:12 Finished candle/overloading/semantics                         26m09s   2GB
Nov 04 19:18:12 Starting candle/overloading/monadic
Nov 04 19:23:49 Finished candle/overloading/monadic                            5m36s   1GB
Nov 04 19:23:49 Starting candle/overloading/ml_kernel
Nov 04 19:39:11 Finished candle/overloading/ml_kernel                         15m21s   3GB
Nov 04 19:39:11 Starting candle/overloading/ml_checker
Nov 04 19:44:41 Finished candle/overloading/ml_checker                         5m29s   3GB
Nov 04 19:44:41 Starting candle/prover
Nov 04 19:59:10 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(242s)     OK
Starting work on compute_evalProofTheory
candle_kernel_permsTheory                                                                                                                                                              candle/prover(408s)     OK
compute_evalProofTheory                                                                                                                                                        candle/prover/compute(186s)     OK
Starting work on compute_execProofTheory
compute_execProofTheory                                                                                                                                                        candle/prover/compute (29s)     OK
Starting work on computeProofTheory
computeProofTheory                                                                                                                                                             candle/prover/compute(119s)     OK
Finished $(CAKEMLDIR)/candle/prover/compute [#theories: 4]                                                                                                                                             (577.872s) 
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                                                                                                                                               candle/prover(170s)     OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory                                                                                                                                                           candle/prover (92s)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"}