CakeML:e478de77a5255174e482f2b80da2b0edd1ad95d1
Add a heap to embody misc; use it in semantics
#855 (minor-reheapification)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
Merge pull request #852 from CakeML/tidy-up
HOL:288eed203f9e91e52a1707519ea31e41041b2f48
Move more examples into parallel build process
Machine:oven3+4.19.67.1.amd64-smp+
Claimed job
Reusing+HOL
Starting+developers
Finished+developers++++++++++++++++++++++++++++++++++++++++7.86+109396
Starting+developers/bin
Finished+developers/bin++++++++++++++++++++++++++++++++++++10.06+685536
Starting+semantics/ffi
Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++18.91+248192
Starting+semantics
Finished+semantics+++++++++++++++++++++++++++++++++++++++++191.25+996696
Starting+semantics/proofs
Finished+semantics/proofs++++++++++++++++++++++++++++++++++462.04+1143312
Starting+semantics/alt_semantics
Finished+semantics/alt_semantics+++++++++++++++++++++++++++27.36+384364
Starting+semantics/alt_semantics/proofs
Finished+semantics/alt_semantics/proofs++++++++++++++++++++307.99+1201524
Starting+basis/pure
Finished+basis/pure++++++++++++++++++++++++++++++++++++++++103.81+911464
Starting+translator
Finished+translator++++++++++++++++++++++++++++++++++++++++346.24+1855812
Starting+compiler/parsing
Finished+compiler/parsing++++++++++++++++++++++++++++++++++157.62+3058780
Starting+characteristic
Finished+characteristic++++++++++++++++++++++++++++++++++++710.28+1979236
Starting+translator/monadic
Finished+translator/monadic++++++++++++++++++++++++++++++++205.56+1496616
Starting+basis
Finished+basis+++++++++++++++++++++++++++++++++++++++++++++5970.16+13754640
Starting+compiler/inference
Finished+compiler/inference++++++++++++++++++++++++++++++++144.76+956344
Starting+compiler/backend/reg_alloc
Finished+compiler/backend/reg_alloc++++++++++++++++++++++++123.59+1265916
Starting+compiler/backend/gc
Finished+compiler/backend/gc+++++++++++++++++++++++++++++++396.95+1705812
Starting+compiler/backend
Finished+compiler/backend++++++++++++++++++++++++++++++++++524.95+2632232
Starting+compiler/encoders/asm
Finished+compiler/encoders/asm+++++++++++++++++++++++++++++47.86+653704
Starting+compiler/encoders/x64
Finished+compiler/encoders/x64+++++++++++++++++++++++++++++54.94+989468
Starting+compiler/encoders/arm7
Finished+compiler/encoders/arm7++++++++++++++++++++++++++++115.18+781668
Starting+compiler/encoders/arm8
Finished+compiler/encoders/arm8++++++++++++++++++++++++++++28.93+919628
Starting+compiler/encoders/mips
Finished+compiler/encoders/mips++++++++++++++++++++++++++++37.51+979328
Starting+compiler/encoders/riscv
Finished+compiler/encoders/riscv+++++++++++++++++++++++++++33.12+715672
Starting+compiler/encoders/ag32
Finished+compiler/encoders/ag32++++++++++++++++++++++++++++38.40+609732
Starting+compiler/backend/x64
Finished+compiler/backend/x64++++++++++++++++++++++++++++++42.20+1428624
Starting+compiler/backend/arm7
Finished+compiler/backend/arm7+++++++++++++++++++++++++++++43.18+1331908
Starting+compiler/backend/arm8
Finished+compiler/backend/arm8+++++++++++++++++++++++++++++41.96+1328456
Starting+compiler/backend/mips
Finished+compiler/backend/mips+++++++++++++++++++++++++++++41.82+1396996
Starting+compiler/backend/riscv
Finished+compiler/backend/riscv++++++++++++++++++++++++++++40.99+1457660
Starting+compiler/backend/ag32
Finished+compiler/backend/ag32+++++++++++++++++++++++++++++144.00+1336508
Starting+compiler/parsing/proofs
Finished+compiler/parsing/proofs+++++++++++++++++++++++++++498.54+1225084
Starting+compiler/inference/proofs
Finished+compiler/inference/proofs+++++++++++++++++++++++++316.21+1314348
Starting+compiler/backend/semantics
Finished+compiler/backend/semantics++++++++++++++++++++++++3608.22+2072932
Starting+compiler/backend/reg_alloc/proofs
Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++449.01+955104
Starting+compiler/backend/proofs
FAILED:+compiler/backend/proofs
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)/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/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Finished $(CAKEMLDIR)/misc (0.000s)
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
README.md compiler/backend/proofs (2s) OK
Starting work on data_spaceProofTheory
data_simpProofTheory compiler/backend/proofs (27s) OK
Starting work on bvl_constProofTheory
data_spaceProofTheory compiler/backend/proofs (52s) OK
Starting work on bvi_letProofTheory
bvi_letProofTheory compiler/backend/proofs (31s) OK
Starting work on clos_annotateProofTheory
clos_annotateProofTheory compiler/backend/proofs (47s) OK
Starting work on clos_callProofTheory
data_liveProofTheory compiler/backend/proofs(142s) OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory compiler/backend/proofs(194s) OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory compiler/backend/proofs (33s) OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory compiler/backend/proofs (55s) OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory compiler/backend/proofs (27s) OK
Starting work on clos_knownPropsTheory
bvi_tailrecProofTheory compiler/backend/proofs(346s) OK
Starting work on bvl_to_bviProofTheory
clos_knownPropsTheory compiler/backend/proofs (18s) OK
Starting work on clos_letopProofTheory
clos_letopProofTheory compiler/backend/proofs (30s) OK
Starting work on clos_opProofTheory
bvi_to_dataProofTheory compiler/backend/proofs(249s) OK
Starting work on clos_ticksProofTheory
clos_opProofTheory compiler/backend/proofs (43s) OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory compiler/backend/proofs (43s) OK
Starting work on clos_knownProofTheory
clos_callProofTheory compiler/backend/proofs(307s) OK
Starting work on clos_numberProofTheory
clos_numberProofTheory compiler/backend/proofs (51s) OK
Starting work on bvl_jumpProofTheory
clos_mtiProofTheory compiler/backend/proofs (64s) OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory compiler/backend/proofs (16s) OK
Starting work on word_bignumProofTheory
word_simpProofTheory compiler/backend/proofs (98s) OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory compiler/backend/proofs (51s) OK
Starting work on data_to_word_memoryProofTheory
clos_knownProofTheory compiler/backend/proofs(253s) OK
Starting work on clos_to_bvlProofTheory
bvl_to_bviProofTheory compiler/backend/proofs(353s) OK
Starting work on word_allocProofTheory
word_bignumProofTheory compiler/backend/proofs(376s) OK
Starting work on word_instProofTheory
word_instProofTheory compiler/backend/proofs (92s) OK
Starting work on word_removeProofTheory
word_removeProofTheory compiler/backend/proofs (52s) OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory compiler/backend/proofs(373s) OK
Starting work on flat_patternProofTheory
flat_patternProofTheory compiler/backend/proofs (76s) OK
Starting work on flat_to_closProofTheory
word_depthProofTheory compiler/backend/proofs(123s) OK
Starting work on lab_filterProofTheory
lab_filterProofTheory compiler/backend/proofs(113s) OK
Starting work on stack_removeProofTheory
flat_to_closProofTheory compiler/backend/proofs(147s) OK
Starting work on source_evalProofTheory
source_evalProofTheory compiler/backend/proofs (57s)FAIL<1>
Exception raised at TotalDefn.xDefine:
at Defn.Hol_defn:
between line 1347, character 2 and line 1359, character 14:
at Defn.prim_mk_defn:
Simple definition failed with message: Definition.new_definition: at Thm.new_specification:
Free variables in rhs of definition: "shift_seq"
error in quse /root/regression/cakeml-1707/compiler/backend/proofs/source_evalProofScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1347, character 2 and line 1359, character 14:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"shift_seq\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
error in load /root/regression/cakeml-1707/compiler/backend/proofs/source_evalProofScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1347, character 2 and line 1359, character 14:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"shift_seq\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1347, character 2 and line 1359, character 14:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"shift_seq\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
data_to_word_memoryProofTheory compiler/backend/proofs(698s)MKILLED
word_allocProofTheory compiler/backend/proofs(660s)MKILLED
stack_removeProofTheory compiler/backend/proofs (76s)MKILLED