CakeML:874bb72cf49d4a806eb88215b31da518ea5352f8
Delay building of L3 equivalence proofs until needed
#858 (asl-equiv)
Merging into:5525b2dc1da264a4ad4d5b5dd23599b8fe8bafe3
Use Definition.new_definition
HOL:4cf5152547dba4db8875c3221511ca11e364ed9c
Fix more Holmakefiles for unlikely parallel build scenarios
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 92MB
Starting developers/bin
Finished developers/bin 4s 674MB
Starting semantics/ffi
Finished semantics/ffi 9s 212MB
Starting semantics
Finished semantics 1m34s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m31s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 12s 346MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m25s 1GB
Starting basis/pure
Finished basis/pure 2m45s 686MB
Starting translator
Finished translator 2m52s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m14s 2GB
Starting characteristic
Finished characteristic 5m48s 2GB
Starting translator/monadic
Finished translator/monadic 1m54s 1GB
Starting basis
Finished basis 46m10s 16GB
Starting compiler/inference
Finished compiler/inference 1m16s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m08s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m39s 1GB
Starting compiler/backend
FAILED: compiler/backend
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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[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)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[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$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 38 directories
Starting work on spt_closureTheory
Starting work on pattern_commonTheory
Starting work on README.md
Starting work on bviTheory
README.md compiler/backend (0s) OK
Starting work on data_liveTheory
spt_closureTheory examples/algorithms (1s) OK
Finished $(HOLDIR)/examples/algorithms [#theories: 1] (1.640s)
Starting work on data_simpTheory
pattern_commonTheory compiler/backend/pattern_matching (7s) OK
Starting work on pattern_semanticsTheory
bviTheory compiler/backend (10s) OK
Starting work on data_spaceTheory
data_simpTheory compiler/backend (10s) OK
Starting work on bvi_letTheory
data_liveTheory compiler/backend (14s) OK
Starting work on bvi_tailrecTheory
pattern_semanticsTheory compiler/backend/pattern_matching (12s) OK
Starting work on pattern_compTheory
bvi_letTheory compiler/backend (10s) OK
Starting work on bvlTheory
data_spaceTheory compiler/backend (14s) OK
Starting work on bvi_to_dataTheory
pattern_compTheory compiler/backend/pattern_matching (14s) OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (33.840s)
Starting work on db_varsTheory
bvlTheory compiler/backend (10s) OK
Starting work on bvl_constTheory
bvi_to_dataTheory compiler/backend (17s) OK
Starting work on bvl_jumpTheory
db_varsTheory compiler/backend (10s) OK
Starting work on clos_annotateTheory
bvl_jumpTheory compiler/backend (10s) OK
Starting work on clos_callTheory
bvi_tailrecTheory compiler/backend (41s) OK
Starting work on clos_fvsTheory
clos_annotateTheory compiler/backend (13s) OK
Starting work on clos_letopTheory
clos_fvsTheory compiler/backend (10s) OK
Starting work on clos_opTheory
clos_callTheory compiler/backend (14s) OK
Starting work on clos_ticksTheory
clos_letopTheory compiler/backend (11s) OK
Starting work on clos_mtiTheory
clos_ticksTheory compiler/backend (10s) OK
Starting work on clos_numberTheory
clos_mtiTheory compiler/backend (13s) OK
Starting work on flatLangTheory
clos_numberTheory compiler/backend (10s) OK
Starting work on jsonLangTheory
bvl_constTheory compiler/backend (64s) OK
Starting work on bvl_handleTheory
flatLangTheory compiler/backend (16s) OK
Starting work on flat_to_closTheory
clos_opTheory compiler/backend (36s) OK
Starting work on clos_knownTheory
jsonLangTheory compiler/backend (11s) OK
Starting work on labLangTheory
bvl_handleTheory compiler/backend (13s) OK
Starting work on bvl_inlineTheory
labLangTheory compiler/backend (11s) OK
Starting work on lab_filterTheory
clos_knownTheory compiler/backend (13s)FAIL<1>
Exception raised at Tactical.FIRST_ASSUM:
Exception raised at TotalDefn.tDefine:
at Defn.tprove:
at Tactical.FIRST_ASSUM:
error in quse /home/cug/hk324/cml-regression/cakeml-1755/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/cug/hk324/cml-regression/cakeml-1755/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"}
flat_to_closTheory compiler/backend (15s)MKILLED
bvl_inlineTheory compiler/backend (5s)MKILLED
lab_filterTheory compiler/backend (0s)MKILLED