CakeML:874bb72cf49d4a806eb88215b31da518ea5352f8
Delay building of L3 equivalence proofs until needed
#858 (asl-equiv)
Merging into:5525b2dc1da264a4ad4d5b5dd23599b8fe8bafe3
Use Definition.new_definition
HOL:1cb031bd28388f55c032c31177684989f80eda10
emacs-mode: cope with deletion of copy-region-as-hol-definition-quietly
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 151MB
Starting developers/bin
Finished developers/bin 5s 670MB
Starting semantics/ffi
Finished semantics/ffi 9s 234MB
Starting semantics
Finished semantics 1m30s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m52s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 13s 364MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m40s 777MB
Starting basis/pure
Finished basis/pure 54s 983MB
Starting translator
Finished translator 3m03s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m20s 2GB
Starting characteristic
Finished characteristic 6m11s 1GB
Starting translator/monadic
Finished translator/monadic 1m50s 1GB
Starting basis
Finished basis 50m24s 13GB
Starting compiler/inference
Finished compiler/inference 1m13s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m10s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m47s 1GB
Starting compiler/backend
FAILED: compiler/backend
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
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)/semantics/proofs
Scanned 38 directories
Starting work on pattern_commonTheory
Starting work on README.md
Starting work on bviTheory
Starting work on data_liveTheory
README.md compiler/backend (0s) OK
Starting work on data_simpTheory
pattern_commonTheory compiler/backend/pattern_matching (8s) OK
Starting work on pattern_semanticsTheory
bviTheory compiler/backend (11s) OK
Starting work on data_spaceTheory
data_simpTheory compiler/backend (11s) OK
Starting work on bvi_letTheory
data_liveTheory compiler/backend (15s) OK
Starting work on bvi_tailrecTheory
pattern_semanticsTheory compiler/backend/pattern_matching (13s) OK
Starting work on pattern_compTheory
bvi_letTheory compiler/backend (11s) OK
Starting work on bvlTheory
data_spaceTheory compiler/backend (16s) OK
Starting work on bvi_to_dataTheory
bvlTheory compiler/backend (11s) OK
Starting work on bvl_constTheory
pattern_compTheory compiler/backend/pattern_matching (15s) OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (37.011s)
Starting work on db_varsTheory
bvi_to_dataTheory compiler/backend (18s) OK
Starting work on bvl_jumpTheory
db_varsTheory compiler/backend (11s) OK
Starting work on clos_annotateTheory
bvl_jumpTheory compiler/backend (11s) OK
Starting work on clos_callTheory
bvi_tailrecTheory compiler/backend (46s) OK
Starting work on clos_fvsTheory
clos_annotateTheory compiler/backend (14s) OK
Starting work on clos_letopTheory
clos_fvsTheory compiler/backend (11s) OK
Starting work on clos_opTheory
clos_callTheory compiler/backend (15s) OK
Starting work on clos_ticksTheory
clos_letopTheory compiler/backend (12s) OK
Starting work on clos_mtiTheory
clos_ticksTheory compiler/backend (10s) OK
Starting work on clos_numberTheory
clos_mtiTheory compiler/backend (14s) OK
Starting work on flatLangTheory
clos_numberTheory compiler/backend (11s) OK
Starting work on jsonLangTheory
bvl_constTheory compiler/backend (73s) OK
Starting work on bvl_handleTheory
flatLangTheory compiler/backend (18s) OK
Starting work on flat_to_closTheory
jsonLangTheory compiler/backend (13s) OK
Starting work on labLangTheory
clos_opTheory compiler/backend (40s) OK
Starting work on clos_knownTheory
bvl_handleTheory compiler/backend (15s) OK
Starting work on bvl_inlineTheory
labLangTheory compiler/backend (12s) OK
Starting work on lab_filterTheory
flat_to_closTheory compiler/backend (17s) OK
Starting work on displayLangTheory
clos_knownTheory compiler/backend (15s)FAIL<1>
Exception raised at Tactical.FIRST_ASSUM:
Exception raised at TotalDefn.tDefine:
at Defn.tprove:
at Tactical.FIRST_ASSUM:
error in quse /home/cake/oven/regression/cakeml-1760/compiler/backend/clos_knownScript.sml : HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
error in load /home/cake/oven/regression/cakeml-1760/compiler/backend/clos_knownScript : HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
Uncaught exception: HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
bvl_inlineTheory compiler/backend (5s)MKILLED
lab_filterTheory compiler/backend (2s)MKILLED
displayLangTheory compiler/backend (0s)MKILLED