CakeML Regression Test

Job 2840

CakeML:f3bab934b78f47b913d62379dd17e6e3568efa09
  nondet example simplified [May 27 16:48:17]
#1183 (scheme)
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 30 11:02:52 Claimed job
May 30 11:03:00 Reusing HOL
May 30 11:03:10 Starting developers
May 30 11:03:14 Finished developers                                               3s 208MB
May 30 11:03:15 Starting developers/bin
May 30 11:03:21 Finished developers/bin                                           4s 592MB
May 30 11:03:22 Starting misc
May 30 11:04:02 Finished misc                                                    39s   1GB
May 30 11:04:03 Starting compiler/proofs
May 30 11:05:02 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 balanced_mapTheory
Starting work on ffiTheory
Starting work on fpValTreeTheory
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
tokensTheory                                             semantics  (3s)     OK
Starting work on gramTheory
ffiTheory                                            semantics/ffi  (6s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                     (6.830s) 
Starting work on tokenUtilsTheory
fpSemTheory                                              semantics  (1s)     OK
Starting work on astTheory
tokenUtilsTheory                                         semantics  (7s)     OK
Starting work on lexer_funTheory
gramTheory                                               semantics  (7s)     OK
Starting work on mllistTheory
astTheory                                                semantics  (7s)     OK
Starting work on semanticPrimitivesTheory
mllistTheory                                            basis/pure  (2s)     OK
Starting work on cmlPtreeConversionTheory
cmlPtreeConversionTheory                                 semantics (19s)     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-2840/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-2840/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 (51s)MKILLED
lexer_funTheory                                          semantics (35s)MKILLED
mlstringTheory                                          basis/pure  (9s)MKILLED