CakeML:b6ce1417ef4a3913736824d1853fa54db032c681
Merge branch 'master' into minor-reheapification
#855 (minor-reheapification)
Merging into:5525b2dc1da264a4ad4d5b5dd23599b8fe8bafe3
Use Definition.new_definition
HOL:4cf5152547dba4db8875c3221511ca11e364ed9c
Fix more Holmakefiles for unlikely parallel build scenarios
Machine:oven3+4.19.67.1.amd64-smp+
Claimed job
Reusing+HOL
Starting+developers
Finished+developers++++++++++++++++++++++++++++++++++++++++8.14+133304
Starting+developers/bin
Finished+developers/bin++++++++++++++++++++++++++++++++++++9.69+674040
Starting+semantics/ffi
Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++24.04+256064
Starting+semantics
Finished+semantics+++++++++++++++++++++++++++++++++++++++++204.18+1140520
Starting+semantics/proofs
Finished+semantics/proofs++++++++++++++++++++++++++++++++++468.32+1185316
Starting+semantics/alt_semantics
Finished+semantics/alt_semantics+++++++++++++++++++++++++++29.72+445144
Starting+semantics/alt_semantics/proofs
Finished+semantics/alt_semantics/proofs++++++++++++++++++++312.87+1548788
Starting+basis/pure
Finished+basis/pure++++++++++++++++++++++++++++++++++++++++108.36+699188
Starting+translator
Finished+translator++++++++++++++++++++++++++++++++++++++++360.21+1492180
Starting+compiler/parsing
Finished+compiler/parsing++++++++++++++++++++++++++++++++++164.54+2647364
Starting+characteristic
Finished+characteristic++++++++++++++++++++++++++++++++++++744.32+2600984
Starting+translator/monadic
Finished+translator/monadic++++++++++++++++++++++++++++++++226.94+1852336
Starting+basis
Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6069.26+26633788
Starting+compiler/inference
Finished+compiler/inference++++++++++++++++++++++++++++++++164.63+1231056
Starting+compiler/backend/reg_alloc
Finished+compiler/backend/reg_alloc++++++++++++++++++++++++134.41+1554316
Starting+compiler/backend/gc
Finished+compiler/backend/gc+++++++++++++++++++++++++++++++447.65+1698772
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 (3s) OK
Finished $(HOLDIR)/examples/algorithms [#theories: 1] (3.255s)
Starting work on data_simpTheory
pattern_commonTheory compiler/backend/pattern_matching (17s) OK
Starting work on pattern_semanticsTheory
bviTheory compiler/backend (22s) OK
Starting work on data_spaceTheory
data_simpTheory compiler/backend (22s) OK
Starting work on bvi_letTheory
data_liveTheory compiler/backend (32s) OK
Starting work on bvi_tailrecTheory
pattern_semanticsTheory compiler/backend/pattern_matching (21s) OK
Starting work on pattern_compTheory
bvi_letTheory compiler/backend (21s) OK
Starting work on bvlTheory
data_spaceTheory compiler/backend (28s) OK
Starting work on bvi_to_dataTheory
pattern_compTheory compiler/backend/pattern_matching (27s) OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (66.932s)
Starting work on db_varsTheory
bvlTheory compiler/backend (19s) OK
Starting work on bvl_constTheory
bvi_to_dataTheory compiler/backend (33s) OK
Starting work on bvl_jumpTheory
db_varsTheory compiler/backend (19s) OK
Starting work on clos_annotateTheory
bvl_jumpTheory compiler/backend (19s) OK
Starting work on clos_callTheory
clos_annotateTheory compiler/backend (24s) OK
Starting work on clos_fvsTheory
bvi_tailrecTheory compiler/backend (81s) OK
Starting work on clos_letopTheory
clos_callTheory compiler/backend (24s) OK
Starting work on clos_opTheory
clos_fvsTheory compiler/backend (19s) OK
Starting work on clos_ticksTheory
clos_letopTheory compiler/backend (21s) OK
Starting work on clos_mtiTheory
clos_ticksTheory compiler/backend (18s) OK
Starting work on clos_numberTheory
clos_mtiTheory compiler/backend (25s) OK
Starting work on flatLangTheory
clos_numberTheory compiler/backend (19s) OK
Starting work on jsonLangTheory
jsonLangTheory compiler/backend (20s) OK
Starting work on labLangTheory
flatLangTheory compiler/backend (30s) OK
Starting work on flat_to_closTheory
bvl_constTheory compiler/backend(129s) OK
Starting work on bvl_handleTheory
clos_opTheory compiler/backend (69s) OK
Starting work on clos_knownTheory
labLangTheory compiler/backend (23s) OK
Starting work on lab_filterTheory
bvl_handleTheory compiler/backend (27s) OK
Starting work on bvl_inlineTheory
flat_to_closTheory compiler/backend (30s) OK
Starting work on displayLangTheory
clos_knownTheory compiler/backend (27s)FAIL<1>
Exception raised at Tactical.FIRST_ASSUM:
Exception raised at TotalDefn.tDefine:
at Defn.tprove:
at Tactical.FIRST_ASSUM:
error in quse /root/regression/cakeml-1754/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 /root/regression/cakeml-1754/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"}
lab_filterTheory compiler/backend (8s)MKILLED
bvl_inlineTheory compiler/backend (3s)MKILLED
displayLangTheory compiler/backend (1s)MKILLED