OverviewCakeML:cd843a232b547bd11e4ee72951e4eaaa9e4ada0b
Future-proof misc (to work with HOL develop and master)
HOL:511e4a42e7cb57caffe27cfa441825baa744d7ec
Update src for strip_binop change
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 105MB
Starting developers/bin
Finished developers/bin 7s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 218MB
Starting semantics
Finished semantics 1m32s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m45s 944MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 9s 341MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m21s 872MB
Starting basis/pure
Finished basis/pure 3m18s 857MB
Starting translator
Finished translator 2m57s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m25s 2GB
Starting characteristic
Finished characteristic 6m30s 2GB
Starting translator/monadic
Finished translator/monadic 1m47s 1GB
Starting basis
Finished basis 36m40s 17GB
Starting compiler/inference
Finished compiler/inference 1m16s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m10s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 4m14s 2GB
Starting compiler/backend
Finished compiler/backend 5m29s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 24s 748MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m06s 761MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m06s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 40s 880MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m26s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m42s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 19s 656MB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 21s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 20s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 19s 893MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m18s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m10s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m47s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 34m25s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m51s 886MB
Starting compiler/backend/proofs
FAILED: compiler/backend/proofs
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md real: 1s user: 1s OK
Starting work on data_simpProofTheory
reachable_sptProofTheory real: 15s user: 14s OK
Starting work on data_spaceProofTheory
data_simpProofTheory real: 17s user: 16s OK
Starting work on bvl_constProofTheory
data_spaceProofTheory real: 35s user: 34s OK
Starting work on bvi_letProofTheory
bvi_letProofTheory real: 26s user: 25s OK
Starting work on clos_annotateProofTheory
data_liveProofTheory real: 87s user: 85s OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory real: 68s user: 66s OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory real: 34s user: 33s OK
Starting work on clos_callProofTheory
bvl_handleProofTheory real: 25s user: 24s OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory real: 43s user: 42s OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory real: 26s user: 25s OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory real: 15s user: 14s OK
Starting work on clos_letopProofTheory
clos_letopProofTheory real: 21s user: 20s OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory real: 232s user: 228s OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory real: 34s user: 32s OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory real: 175s user: 171s OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory real: 51s user: 49s OK
Starting work on clos_numberProofTheory
clos_numberProofTheory real: 15s user: 13sFAIL<1>
EVERY ($<= n) (code_locs [SND (renumber_code_locs n e)])
EVERY ($> (FST (renumber_code_locs n e)))
(code_locs [SND (renumber_code_locs n e)])
failed.
First unsolved sub-goal is
SORTED $< (code_locs (r::r''))
Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
clos_callProofTheory M-KILLED
bvl_to_bviProofTheory M-KILLED
clos_knownProofTheory M-KILLED