CakeML Regression Test

Job 2819

CakeML:2cb913bafb3f7b8bc061e5c7001747bf1c7f018e
  remove duplicate lemma [May 05 20:10:54]
#1165 (pancake_internal32bit)
Merging into:901170b785fb177d23b8f92318e9252266eed3ac
  Merge pull request #1161 from CakeML/untime [May 06 06:39:04]
HOL:ef2577146c81145e97682d40efb1dbbd17366dcd
  Further progress with pi-calculus recursion principle [May 02 00:59:57]
Machine:pavlova

May 06 07:02:57 Claimed job
May 06 07:03:05 Building HOL
May 06 07:13:53 Starting developers
May 06 07:13:57 Finished developers                                               3s 223MB
May 06 07:13:58 Starting developers/bin
May 06 07:14:03 Finished developers/bin                                           4s 591MB
May 06 07:14:04 Starting misc
May 06 07:15:03 Finished misc                                                    57s   2GB
May 06 07:15:04 Starting compiler/proofs
May 06 07:16:52 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/ring/src
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 92 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.060s) 
Starting work on charsetTheory
NTpropertiesTheory          examples/formal-languages/context-free  (4s)     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
temporalTheory                  examples/machine-code/hoare-triple  (2s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]   (2.940s) 
Starting work on ffiTheory
simpleSexpPEGTheory         examples/formal-languages/context-free  (3s)     OK
Starting work on simpleSexpParseTheory
charsetTheory                    examples/formal-languages/regular  (8s)     OK
Starting work on regexpTheory
ffiTheory                                            semantics/ffi  (7s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                     (7.660s) 
Starting work on fpValTreeTheory
fpValTreeTheory                                          semantics  (1s)     OK
Starting work on fpOptTheory
simpleSexpParseTheory       examples/formal-languages/context-free (10s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (22.990s) 
Starting work on namespaceTheory
namespaceTheory                                          semantics  (2s)     OK
Starting work on realOpsTheory
realOpsTheory                                            semantics  (1s)     OK
Starting work on tokensTheory
fpOptTheory                                              semantics  (4s)     OK
Starting work on fpSemTheory
regexpTheory                     examples/formal-languages/regular (14s)     OK
Starting work on mllistTheory
fpSemTheory                                              semantics  (1s)     OK
Starting work on astTheory
tokensTheory                                             semantics  (3s)     OK
Starting work on gramTheory
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 (19s)     OK
Starting work on mlstringTheory
semanticPrimitivesTheory                                 semantics (34s)     OK
Starting work on evaluateTheory
mlstringTheory                                          basis/pure (12s)     OK
Starting work on typeSystemTheory
lexer_funTheory                                          semantics (39s)     OK
Starting work on mlintTheory
evaluateTheory                                           semantics  (5s)     OK
Starting work on mloptionTheory
mloptionTheory                                          basis/pure  (2s)     OK
Starting work on astPropsTheory
astPropsTheory                                    semantics/proofs  (1s)     OK
Starting work on gramPropsTheory
mlintTheory                                             basis/pure  (7s)     OK
Starting work on mlratTheory
typeSystemTheory                                         semantics (13s)     OK
Starting work on primTypesTheory
mlratTheory                                             basis/pure  (3s)     OK
Starting work on typeDecToPPTheory
primTypesTheory                                          semantics  (2s)     OK
Starting work on semanticsTheory
typeDecToPPTheory                                       basis/pure  (2s)     OK
Starting work on namespacePropsTheory
semanticsTheory                                          semantics  (4s)     OK
Finished $(CAKEMLDIR)/semantics [#theories: 16]                      (155.160s) 
Starting work on fpOptPropsTheory
namespacePropsTheory                              semantics/proofs  (5s)     OK
Starting work on semanticPrimitivesPropsTheory
gramPropsTheory                                   semantics/proofs (14s)     OK
Starting work on typeSoundInvariantsTheory
fpOptPropsTheory                                  semantics/proofs  (3s)FAIL<1>
 <<HOL message: Created theory "fpOptProps">>
 Saved theorem _______ "substLookup_substUpdate"
 Saved theorem _______ "substUpdate_substLookup"
 Saved theorem _______ "substLookup_substUpdate_alt"
 Saved theorem _______ "substLookup_substAdd_alt"
 Saved theorem _______ "matchWordTree_preserving"
 Saved theorem _______ "matchBoolTree_preserving"
 Saved definition ____ "substMonotone_def"
 Saved theorem _______ "instWordTree_weakening"
 Saved theorem _______ "instBoolTree_weakening"
 Saved theorem _______ "subst_pat_is_word"
 Saved theorem _______ "subst_pat_is_bool"
 Saved theorem _______ "app_match_sym_word"
 Saved theorem _______ "app_match_sym_bool"
 Saved theorem _______ "nth_EL"
 Saved theorem _______ "EL_nth"
 Saved theorem _______ "rwAllWordTree_empty_rewrites"
 Saved theorem _______ "rwAllBoolTree_empty_rewrites"
 Saved theorem _______ "rwAllWordTree_id"
 Saved theorem _______ "rwAllBoolTree_id"
 Saved theorem _______ "rwAllWordTree_up"
 Saved theorem _______ "rwAllBoolTree_up"
 Saved theorem _______ "rwAllWordTree_comp_unop"
 Saved theorem _______ "rwAllWordTree_comp_right"
 Saved theorem _______ "rwAllWordTree_comp_left"
 Saved theorem _______ "rwAllWordTree_comp_terop_l"
 Saved theorem _______ "rwAllWordTree_comp_terop_r"
 Saved theorem _______ "rwAllWordTree_comp_terop_c"
 Proof of 
 
 sc v vres insts rws t.
   rwAllWordTree insts rws v = SOME vres 
   insts_new.
     rwAllWordTree insts_new rws (Fp_wopt sc v) = SOME (Fp_wopt sc vres)
 
 failed.
 Failed to prove theorem rwAllWordTree_comp_scope_T.
 
 Exception raised at Tactical.FIRST_ASSUM:
 
 error in quse /scratch/cakeml/regression/cakeml-2819/semantics/proofs/fpOptPropsScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2819/semantics/proofs/fpOptPropsScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-ef2577146c81145e97682d40efb1dbbd17366dcd/src/prekernel/Feedback.sml:124: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical", source_location = Loc_Unknown}
balanced_mapTheory                           examples/balanced_bst (98s)MKILLED
semanticPrimitivesPropsTheory                     semantics/proofs  (0s)MKILLED
typeSoundInvariantsTheory                         semantics/proofs  (0s)MKILLED