CakeML: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.17+156724
Starting+developers/bin
Finished+developers/bin++++++++++++++++++++++++++++++++++++9.56+680316
Starting+semantics/ffi
Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++22.61+245784
Starting+semantics
Finished+semantics+++++++++++++++++++++++++++++++++++++++++174.09+1174128
Starting+semantics/proofs
Finished+semantics/proofs++++++++++++++++++++++++++++++++++473.69+1324872
Starting+semantics/alt_semantics
Finished+semantics/alt_semantics+++++++++++++++++++++++++++28.68+415136
Starting+semantics/alt_semantics/proofs
Finished+semantics/alt_semantics/proofs++++++++++++++++++++321.46+995824
Starting+basis/pure
Finished+basis/pure++++++++++++++++++++++++++++++++++++++++106.22+675860
Starting+translator
Finished+translator++++++++++++++++++++++++++++++++++++++++353.70+1945800
Starting+compiler/parsing
Finished+compiler/parsing++++++++++++++++++++++++++++++++++160.33+3336164
Starting+characteristic
Finished+characteristic++++++++++++++++++++++++++++++++++++749.63+2340836
Starting+translator/monadic
Finished+translator/monadic++++++++++++++++++++++++++++++++222.88+1474144
Starting+basis
Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6049.79+19335312
Starting+compiler/inference
Finished+compiler/inference++++++++++++++++++++++++++++++++146.57+1214524
Starting+compiler/backend/reg_alloc
Finished+compiler/backend/reg_alloc++++++++++++++++++++++++125.74+1540400
Starting+compiler/backend/gc
Finished+compiler/backend/gc+++++++++++++++++++++++++++++++416.11+1676492
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 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 (17s) OK
Starting work on pattern_semanticsTheory
data_simpTheory compiler/backend (23s) OK
Starting work on data_spaceTheory
bviTheory compiler/backend (24s) OK
Starting work on bvi_letTheory
data_liveTheory compiler/backend (28s) OK
Starting work on bvi_tailrecTheory
pattern_semanticsTheory compiler/backend/pattern_matching (22s) OK
Starting work on pattern_compTheory
bvi_letTheory compiler/backend (21s) OK
Starting work on bvlTheory
data_spaceTheory compiler/backend (29s) OK
Starting work on bvi_to_dataTheory
pattern_compTheory compiler/backend/pattern_matching (25s) OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (64.783s)
Starting work on db_varsTheory
bvlTheory compiler/backend (19s) OK
Starting work on bvl_constTheory
db_varsTheory compiler/backend (19s) OK
Starting work on bvl_jumpTheory
bvi_to_dataTheory compiler/backend (31s) OK
Starting work on clos_annotateTheory
bvl_jumpTheory compiler/backend (17s) OK
Starting work on clos_callTheory
bvi_tailrecTheory compiler/backend (79s) OK
Starting work on clos_fvsTheory
clos_annotateTheory compiler/backend (23s) OK
Starting work on clos_letopTheory
clos_fvsTheory compiler/backend (19s) OK
Starting work on clos_opTheory
clos_callTheory compiler/backend (25s) OK
Starting work on clos_ticksTheory
clos_letopTheory compiler/backend (20s) OK
Starting work on clos_mtiTheory
clos_ticksTheory compiler/backend (19s) OK
Starting work on clos_numberTheory
clos_mtiTheory compiler/backend (27s) OK
Starting work on flatLangTheory
clos_numberTheory compiler/backend (19s) OK
Starting work on jsonLangTheory
bvl_constTheory compiler/backend(125s) OK
Starting work on bvl_handleTheory
flatLangTheory compiler/backend (29s) OK
Starting work on flat_to_closTheory
jsonLangTheory compiler/backend (20s) OK
Starting work on labLangTheory
clos_opTheory compiler/backend (72s) OK
Starting work on clos_knownTheory
bvl_handleTheory compiler/backend (27s) OK
Starting work on bvl_inlineTheory
labLangTheory compiler/backend (24s) OK
Starting work on lab_filterTheory
flat_to_closTheory compiler/backend (30s) OK
Starting work on displayLangTheory
clos_knownTheory compiler/backend (26s)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-1757/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-1757/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 (8s)MKILLED
lab_filterTheory compiler/backend (7s)MKILLED
displayLangTheory compiler/backend (4s)MKILLED