CakeML:7af274d3b4b73ffa37b508ad944106d871d8af02
Fix and speed up linear_scanProof
HOL:b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d
Add some subscript Unicode characters (+, -, =) to emacs bindings
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers/bin
Finished developers/bin 1m13s 916MB
Starting semantics/ffi
Finished semantics/ffi 11s 273MB
Starting semantics
Finished semantics 1m12s 842MB
Starting semantics/proofs
Finished semantics/proofs 2m50s 1GB
Starting basis/pure
Finished basis/pure 50s 682MB
Starting translator
Finished translator 3m01s 845MB
Starting compiler/parsing
Finished compiler/parsing 1m13s 1GB
Starting characteristic
Finished characteristic 2m30s 1GB
Starting translator/monadic
Finished translator/monadic 1m25s 1GB
Starting basis
Finished basis 16m40s 3GB
Starting compiler/inference
Finished compiler/inference 1m23s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 47s 897MB
Starting compiler/backend/gc
Finished compiler/backend/gc 6m21s 1GB
Starting compiler/backend
Finished compiler/backend 3s 18MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 1s 14MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 15s 442MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 45s 483MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 7s 332MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 9s 455MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 8s 432MB
Starting compiler/backend/x64
Finished compiler/backend/x64 18s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 19s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 19s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m55s 875MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m50s 969MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 8m47s 1GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 2m42s 486MB
Starting compiler/backend/proofs
FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/balanced_bst]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-b97e7e9c09f9a3cbc2e810104cffe0c951a1a64d/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
Starting work on heap
heap OK
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
data_simpProofTheory OK
Starting work on bvl_constProofTheory
data_spaceProofTheory OK
Starting work on bvi_letProofTheory
bvi_letProofTheory OK
Starting work on clos_annotateProofTheory
data_liveProofTheory OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory OK
Starting work on clos_callProofTheory
bvl_constProofTheory OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory OK
Starting work on bvl_inlineProofTheory
bvi_to_dataProofTheory OK
Starting work on clos_fvsProofTheory
bvl_inlineProofTheory OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory OK
Starting work on clos_letopProofTheory
clos_fvsProofTheory OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory OK
Starting work on clos_labelsProofTheory
clos_ticksProofTheory OK
Starting work on clos_knownProofTheory
clos_labelsProofTheory OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory OK
Starting work on clos_numberProofTheory
clos_numberProofTheory OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory OK
Starting work on word_simpProofTheory
bvi_tailrecProofTheory OK
Starting work on bvl_to_bviProofTheory
clos_knownProofTheory OK
Starting work on word_bignumProofTheory
word_simpProofTheory OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory OK
Starting work on data_to_word_memoryProofTheory
clos_callProofTheory OK
Starting work on clos_to_bvlProofTheory
bvl_to_bviProofTheory OK
Starting work on word_allocProofTheory
word_bignumProofTheory OK
Starting work on word_instProofTheory
word_instProofTheory OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory OK
Starting work on flat_elimProofTheory
flat_elimProofTheory OK
Starting work on flat_exh_matchProofTheory
word_removeProofTheory OK
Starting work on flat_reorder_matchProofTheory
flat_exh_matchProofTheory OK
Starting work on flat_to_patProofTheory
flat_reorder_matchProofTheory OK
Starting work on flat_uncheck_ctorsProofTheory
flat_uncheck_ctorsProofTheory OK
Starting work on lab_filterProofTheory
data_to_word_memoryProofTheory OK
Starting work on stack_removeProofTheory
lab_filterProofTheory OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory OK
Starting work on source_to_flatProofTheory
flat_to_patProofTheory OK
Starting work on stack_allocProofTheory
source_to_flatProofTheory OK
Starting work on stack_namesProofTheory
stack_namesProofTheory OK
Starting work on word_to_stackProofTheory
stack_removeProofTheory OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory OK
Starting work on word_elimProofTheory
stack_allocProofTheory OK
word_elimProofTheory OK
data_to_word_gcProofTheory OK
Starting work on data_to_word_bignumProofTheory
Starting work on stack_to_labProofTheory
data_to_word_bignumProofTheory FAILED! <1>
i2mw i = (i < 0,[a3])
FLOOKUP t.store (if a then OtherHeap else NextFree) = SOME (Word a2))
(small_int (:) i
w x.
get_var (adjust_var r) t = SOME (Word w)
get_real_addr c t.store w = SOME x a2 = x + bytes_in_word)
failed.
Failed to prove theorem AnyHeader_thm.
Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 464 (THEN1 on line 463) (THEN1 on line 485)", origin_function = "by", origin_structure = "BasicProvers"}
word_to_stackProofTheory M-KILLED
stack_to_labProofTheory M-KILLED