CakeML Regression Test

Job 2836

CakeML:0a75b1ed4674ce7235a691f5c74605aa3cb67cbb
  fix build-sequence [May 20 15:39:57]
#1179 (pmc)
Merging into:6de002aec2cea179d7ccfc484285fe1504919f76
  Merge pull request #1178 from halogentlepersuasion/pan_static_style [May 17 06:44:31]
HOL:ca9276b7cc564969f431f56eb20f48331455eecf
  WIP on figuring out why TypeBase.register_update_fn is not apparently [May 19 13:28:17]
Machine:pavlova

May 21 13:17:02 Claimed job
May 21 13:17:11 Building HOL
May 21 13:27:54 Starting developers
May 21 13:27:58 Finished developers                                               3s 152MB
May 21 13:27:59 Starting developers/bin
May 21 13:28:05 Finished developers/bin                                           5s 592MB
May 21 13:28:05 Starting misc
May 21 13:29:02 Finished misc                                                    55s   1GB
May 21 13:29:03 Starting compiler/proofs
May 21 13:30:21 FAILED: compiler/proofs
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanned 91 directories
Starting work on NTpropertiesTheory
Starting work on simpleSexpTheory
Starting work on balanced_mapTheory
Starting work on FormalLangTheory
FormalLangTheory                         examples/formal-languages  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages [#theories: 1]            (2.030s) 
Starting work on charsetTheory
NTpropertiesTheory          examples/formal-languages/context-free  (5s)     OK
Starting work on vec_mapTheory
simpleSexpTheory            examples/formal-languages/context-free  (5s)     OK
Starting work on simpleSexpPEGTheory
vec_mapTheory                    examples/formal-languages/regular  (1s)     OK
Starting work on temporalTheory
simpleSexpPEGTheory         examples/formal-languages/context-free  (3s)     OK
Starting work on simpleSexpParseTheory
temporalTheory                  examples/machine-code/hoare-triple  (3s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]   (3.150s) 
Starting work on ffiTheory
charsetTheory                    examples/formal-languages/regular  (8s)     OK
Starting work on regexpTheory
ffiTheory                                            semantics/ffi  (7s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                     (7.260s) 
Starting work on fpValTreeTheory
simpleSexpParseTheory       examples/formal-languages/context-free (10s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (23.660s) 
Starting work on namespaceTheory
fpValTreeTheory                                          semantics  (1s)     OK
Starting work on fpOptTheory
namespaceTheory                                          semantics  (2s)     OK
Starting work on realOpsTheory
realOpsTheory                                            semantics  (0s)     OK
Starting work on tokensTheory
fpOptTheory                                              semantics  (4s)     OK
Starting work on fpSemTheory
regexpTheory                     examples/formal-languages/regular (14s)     OK
Starting work on mllistTheory
tokensTheory                                             semantics  (3s)     OK
Starting work on gramTheory
fpSemTheory                                              semantics  (1s)     OK
Starting work on astTheory
mllistTheory                                            basis/pure  (2s)     OK
Starting work on tokenUtilsTheory
astTheory                                                semantics  (7s)     OK
Starting work on semanticPrimitivesTheory
gramTheory                                               semantics  (7s)     OK
Starting work on lexer_funTheory
tokenUtilsTheory                                         semantics  (7s)     OK
Starting work on cmlPtreeConversionTheory
cmlPtreeConversionTheory                                 semantics (20s)     OK
Starting work on mlstringTheory
semanticPrimitivesTheory                                 semantics (31s)FAIL<1>
 Saved induction _____ "maybe_all_list_ind"
 <<HOL message: mk_functional: 
   pattern completion has added 12 clauses to the original specification.>>
 Saved definition ____ "v_to_word8_def"
 Saved definition ____ "v_to_word8_list_def"
 <<HOL message: mk_functional: 
   pattern completion has added 12 clauses to the original specification.>>
 Saved definition ____ "v_to_word64_def"
 Saved definition ____ "v_to_word64_list_def"
 Saved definition ____ "lookup_env_def"
 Saved definition ____ "add_decs_generation_def"
 Saved definition ____ "add_env_generation_def"
 Saved definition ____ "declare_env_def"
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "concrete_v_def"
 Saved induction _____ "concrete_v_ind"
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "compiler_agrees_def"
 <<HOL message: mk_functional: 
   pattern completion has added 16 clauses to the original specification.>>
 Saved definition ____ "do_eval_def"
 <<HOL message: mk_functional: 
   pattern completion has added 3 clauses to the original specification.>>
 Saved definition ____ "reset_env_generation_def"
 Saved definition ____ "copy_array_def"
 Saved definition ____ "ws_to_chars_def"
 Saved definition ____ "chars_to_ws_def"
 Saved definition ____ "opn_lookup_def"
 Saved definition ____ "opb_lookup_def"
 Saved definition ____ "opw8_lookup_def"
 Saved definition ____ "opw64_lookup_def"
 Saved definition ____ "shift8_lookup_def"
 Saved definition ____ "shift64_lookup_def"
 Saved theorem _______ "datatype_exp_or_val"
 Saved theorem _______ "exp_or_val_11"
 Saved theorem _______ "exp_or_val_distinct"
 Saved theorem _______ "exp_or_val_nchotomy"
 Saved theorem _______ "exp_or_val_Axiom"
 Saved theorem _______ "exp_or_val_induction"
 Saved theorem _______ "exp_or_val_case_cong"
 Saved theorem _______ "exp_or_val_case_eq"
 <<HOL message: Defined type: "exp_or_val">>
 <<HOL message: mk_functional: 
   pattern completion has added 15 clauses to the original specification.>>
 Saved definition ____ "do_fprw_def"
 error in quse /scratch/cakeml/regression/cakeml-2836/semantics/semanticPrimitivesScript.sml : HOL_ERR {message = "at goalStack.extract_thm:\nno theorem proved", origin_function = "tprove", origin_structure = "Defn", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2836/semantics/semanticPrimitivesScript : HOL_ERR {message = "at goalStack.extract_thm:\nno theorem proved", origin_function = "tprove", origin_structure = "Defn", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-ca9276b7cc564969f431f56eb20f48331455eecf/src/num/termination/TotalDefn.sml:33: HOL_ERR {message = "at goalStack.extract_thm:\nno theorem proved", origin_function = "tprove", origin_structure = "Defn", source_location = Loc_Unknown}
balanced_mapTheory                           examples/balanced_bst (68s)MKILLED
lexer_funTheory                                          semantics (32s)MKILLED
mlstringTheory                                          basis/pure  (9s)MKILLED