CakeML Regression Test

Job 2255

CakeML:4561273aac7c5290fd1b072cc5090dad1275891d
  ffiname: fix type errors in candle prover due to ffiname change [Dec 16 06:15:41]
#976 (ffiname)
Merging into:4ce61c307e8542262db1b33ca6bbaba2473fd1e0
  Fix linear_scanProof given change in HOL [Dec 13 00:34:12]
HOL:d587e1c70b4c059edc079ed4a529b5b7423223b8
  Add ltree_every and ltree_finite_branching (#1172) [Dec 11 22:22:54]
Machine:pavlova

Dec 16 14:36:45 Claimed job
Dec 16 14:36:49 Reusing HOL
Dec 16 14:36:59 Starting developers
Dec 16 14:37:02 Finished developers                                               2s 224MB
Dec 16 14:37:03 Starting developers/bin
Dec 16 14:37:13 Finished developers/bin                                           8s   1GB
Dec 16 14:37:14 Starting compiler/proofs
Dec 16 16:19:28 Finished compiler/proofs                                    1h42m13s  41GB
Dec 16 16:19:29 Starting compiler/bootstrap/translation
Dec 16 16:21:49 FAILED: compiler/bootstrap/translation
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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[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
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanned 91 directories
Starting work on ml_monadStoreTheory
Starting work on ArrayProofTheory
Starting work on ListProofTheory
Starting work on basis_ffiTheory
ml_monadStoreTheory                             translator/monadic (28s)     OK
Finished $(CAKEMLDIR)/translator/monadic [#theories: 1]               (28.860s) 
Finished $(CAKEMLDIR)/compiler/inference                               (0.000s) 
Starting work on num_list_enc_decTheory
ListProofTheory                                              basis (31s)     OK
Starting work on monadic_encTheory
monadic_encTheory                    compiler/encoders/monadic_enc (16s)     OK
Starting work on monadic_enc32Theory
num_list_enc_decTheory                 compiler/backend/serialiser (26s)     OK
Starting work on num_tree_enc_decTheory
basis_ffiTheory                                              basis (65s)     OK
Starting work on monadic_enc64Theory
monadic_enc32Theory                  compiler/encoders/monadic_enc (21s)     OK
Starting work on caml_lexTheory
ArrayProofTheory                                             basis (76s)     OK
Finished $(CAKEMLDIR)/basis [#theories: 3]                           (174.100s) 
Starting work on lisp_valuesTheory
lisp_valuesTheory                   candle/standard/ml_kernel/lisp  (2s)     OK
Starting work on lisp_parsingTheory
num_tree_enc_decTheory                 compiler/backend/serialiser (20s)     OK
Starting work on backend_enc_decTheory
lisp_parsingTheory                  candle/standard/ml_kernel/lisp  (2s)     OK
Starting work on lisp_printingTheory
lisp_printingTheory                 candle/standard/ml_kernel/lisp  (2s)     OK
Starting work on lisp_parsing_proofsTheory
lisp_parsing_proofsTheory           candle/standard/ml_kernel/lisp  (4s)     OK
Finished $(CAKEMLDIR)/candle/standard/ml_kernel/lisp [#theories: 4]   (11.510s) 
Starting work on holSyntaxLibTheory
monadic_enc64Theory                  compiler/encoders/monadic_enc (21s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]    (59.950s) 
Starting work on ast_extrasTheory
ast_extrasTheory                                     candle/prover (15s)     OK
Starting work on permsTheory
holSyntaxLibTheory                               candle/syntax-lib (16s)     OK
Finished $(CAKEMLDIR)/candle/syntax-lib [#theories: 1]                (16.860s) 
Starting work on holSyntaxTheory
backend_enc_decTheory                  compiler/backend/serialiser (47s)FAIL<1>
 Saved theorem _______ "environment_dec_def"
 Saved theorem _______ "environment_store_enc_def"
 Saved theorem _______ "environment_store_dec_def"
 Saved theorem _______ "source_to_flat_config_enc_def"
 Saved theorem _______ "source_to_flat_config_dec_def"
 Saved theorem _______ "word_to_stack_config_enc_def"
 Saved theorem _______ "word_to_stack_config_dec_def"
 error in quse /scratch/cakeml/regression/cakeml-2255/compiler/backend/serialiser/backend_enc_decScript.sml : HOL_ERR {message = "encode_for_rec failed for :lab_to_target$inc_config", origin_function = "failwith", origin_structure = "??"}
 error in load /scratch/cakeml/regression/cakeml-2255/compiler/backend/serialiser/backend_enc_decScript : HOL_ERR {message = "encode_for_rec failed for :lab_to_target$inc_config", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "encode_for_rec failed for :lab_to_target$inc_config", origin_function = "failwith", origin_structure = "??"}
caml_lexTheory                              compiler/parsing/ocaml (52s)MKILLED
permsTheory                                          candle/prover (20s)MKILLED
holSyntaxTheory                             candle/standard/syntax (21s)MKILLED