CakeML Regression Test

Job 2307

CakeML:f7debdc5449cee693c45ad88940aa3a066188634
  update compileProofTheory for shared memory [Feb 27 02:20:39]
#977 (share_mem_new2)
Merging into:7b2d2fceaca11d0a04487744c515e8b9fcc712cd
  fix cnf_xor infinite loop [Feb 27 04:31:21]
HOL:525694a1f1c7016dea954894bea6e6e396f7d6b3
  HolSmt: add unit tests for circular definitions [Feb 21 23:04:33]
Machine:lammington

Feb 27 04:49:27 Claimed job
Feb 27 04:49:35 Building HOL
Feb 27 05:03:43 Starting developers
Feb 27 05:03:46 Finished developers                                               2s 209MB
Feb 27 05:03:47 Starting developers/bin
Feb 27 05:03:58 Finished developers/bin                                           9s   1GB
Feb 27 05:03:59 Starting compiler/proofs
Feb 27 06:55:19 Finished compiler/proofs                                    1h51m19s  39GB
Feb 27 06:55:20 Starting compiler/bootstrap/translation
Feb 27 06:57:44 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/rational[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 92 directories
Starting work on precparserTheory
Starting work on ml_monadStoreTheory
Starting work on ArrayProofTheory
Starting work on ListProofTheory
precparserTheory            examples/formal-languages/context-free  (1s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1] (1.070s) 
Starting work on basis_ffiTheory
ml_monadStoreTheory                             translator/monadic (29s)     OK
Finished $(CAKEMLDIR)/translator/monadic [#theories: 1]               (29.560s) 
Finished $(CAKEMLDIR)/compiler/inference                               (0.000s) 
Starting work on num_list_enc_decTheory
ListProofTheory                                              basis (32s)     OK
Starting work on monadic_encTheory
monadic_encTheory                    compiler/encoders/monadic_enc (17s)     OK
Starting work on monadic_enc32Theory
num_list_enc_decTheory                 compiler/backend/serialiser (27s)     OK
Starting work on num_tree_enc_decTheory
basis_ffiTheory                                              basis (67s)     OK
Starting work on monadic_enc64Theory
monadic_enc32Theory                  compiler/encoders/monadic_enc (21s)     OK
Starting work on caml_lexTheory
ArrayProofTheory                                             basis (77s)     OK
Finished $(CAKEMLDIR)/basis [#theories: 3]                           (177.410s) 
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 (21s)     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.700s) 
Starting work on holSyntaxLibTheory
monadic_enc64Theory                  compiler/encoders/monadic_enc (22s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]    (60.760s) 
Starting work on ast_extrasTheory
holSyntaxLibTheory                               candle/syntax-lib (16s)     OK
Finished $(CAKEMLDIR)/candle/syntax-lib [#theories: 1]                (16.910s) 
Starting work on holSyntaxTheory
ast_extrasTheory                                     candle/prover (16s)     OK
Starting work on permsTheory
backend_enc_decTheory                  compiler/backend/serialiser (49s)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/regression2/cakeml-2307/compiler/backend/serialiser/backend_enc_decScript.sml : HOL_ERR {message = "at line 442, character 28:\nIncorrect number of arguments to abbreviated operator inc_config (expects 1)", origin_function = "parse_type", origin_structure = "Parse"}
 error in load /scratch/cakeml/regression2/cakeml-2307/compiler/backend/serialiser/backend_enc_decScript : HOL_ERR {message = "at line 442, character 28:\nIncorrect number of arguments to abbreviated operator inc_config (expects 1)", origin_function = "parse_type", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "at line 442, character 28:\nIncorrect number of arguments to abbreviated operator inc_config (expects 1)", origin_function = "parse_type", origin_structure = "Parse"}
caml_lexTheory                              compiler/parsing/ocaml (55s)MKILLED
holSyntaxTheory                             candle/standard/syntax (23s)MKILLED
permsTheory                                          candle/prover (20s)MKILLED