OverviewCakeML:c89761b7ef55823e5883bc0c3b0dd2b5291b05d4
Get some files to build again
HOL:ff3ac4c4c36730c3560764bd9487f22baea5d7a9
Avoid GC test warnings on low user times, and avoid a MoscowML bug
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 34MB
Starting developers/bin
Finished developers/bin 7s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 251MB
Starting semantics
Finished semantics 1m37s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m34s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 339MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m09s 816MB
Starting basis/pure
Finished basis/pure 51s 890MB
Starting translator
Finished translator 2m46s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m20s 3GB
Starting characteristic
Finished characteristic 6m02s 1GB
Starting translator/monadic
Finished translator/monadic 1m39s 1GB
Starting basis
Finished basis 32m55s 11GB
Starting compiler/inference
Finished compiler/inference 1m01s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m02s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m17s 2GB
Starting compiler/backend
Finished compiler/backend 4m34s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 21s 760MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 24s 959MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 50s 650MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 12s 938MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 17s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 15s 926MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 16s 885MB
Starting compiler/backend/x64
Finished compiler/backend/x64 17s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 17s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 18s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 18s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m08s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m30s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m25s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 27m29s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m21s 1GB
Starting compiler/backend/proofs
FAILED: compiler/backend/proofs
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)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[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)/compiler/backend/reachability[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)/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/backend/reachability/proofs[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
Starting work on reachable_sptProofTheory
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
reachable_sptProofTheory real: 12s user: 12s OK
Starting work on data_spaceProofTheory
data_simpProofTheory real: 14s user: 14s OK
Starting work on bvl_constProofTheory
data_spaceProofTheory real: 28s user: 27s OK
Starting work on bvi_letProofTheory
bvi_letProofTheory real: 19s user: 19s OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory real: 52s user: 51s OK
Starting work on bvl_handleProofTheory
data_liveProofTheory real: 71s user: 70s OK
Starting work on bvi_to_dataProofTheory
bvl_handleProofTheory real: 20s user: 20s OK
Starting work on bvl_inlineProofTheory
clos_annotateProofTheory real: 28s user: 27s OK
Starting work on clos_callProofTheory
bvl_inlineProofTheory real: 33s user: 32s OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory real: 19s user: 19s OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory real: 11s user: 11s OK
Starting work on clos_letopProofTheory
clos_letopProofTheory real: 19s user: 18s OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory real: 181s user: 179s OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory real: 25s user: 25s OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory real: 134s user: 132s OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory real: 36s user: 35s OK
Starting work on clos_numberProofTheory
clos_callProofTheory real: 175s user: 173s OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory real: 25s user: 24s OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory real: 10s user: 10s OK
Starting work on word_bignumProofTheory
word_simpProofTheory real: 54s user: 52s OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory real: 130s user: 128s OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory real: 29s user: 29s OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory real: 193s user: 190s OK
Starting work on word_allocProofTheory
word_bignumProofTheory real: 210s user: 207s OK
Starting work on word_instProofTheory
word_instProofTheory real: 51s user: 50s OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory real: 213s user: 210s OK
Starting work on word_depthProofTheory
word_removeProofTheory real: 30s user: 29s OK
Starting work on flat_patternProofTheory
word_depthProofTheory real: 75s user: 73s OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory real: 49s user: 48s OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory real: 57s user: 55s OK
Starting work on stack_removeProofTheory
lab_filterProofTheory real: 60s user: 59s OK
Starting work on flat_elimProofTheory
flat_elimProofTheory real: 73s user: 71s OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory real: 104s user: 103s OK
Starting work on stack_allocProofTheory
stack_removeProofTheory real: 255s user: 252s OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory real: 612s user: 607s OK
Starting work on word_to_wordProofTheory
data_to_word_memoryProofTheory real: 701s user: 697s OK
Starting work on stack_namesProofTheory
word_to_wordProofTheory real: 66s user: 65s OK
Starting work on data_to_word_gcProofTheory
stack_namesProofTheory real: 33s user: 32s OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory real: 72s user: 71s OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory real: 239s user: 236s OK
Starting work on word_elimProofTheory
stack_allocProofTheory real: 425s user: 421s OK
word_elimProofTheory real: 126s user: 124s OK
data_to_word_gcProofTheory real: 244s user: 242s OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory real: 207s user: 205s OK
Starting work on data_to_word_assignProofTheory
data_to_word_assignProofTheory real: 1061s user: 1054s OK
Starting work on data_to_wordProofTheory
word_to_stackProofTheory real: 1619s user: 1603s OK
Starting work on stack_to_labProofTheory
data_to_wordProofTheory real: 224s user: 220s OK
stack_to_labProofTheory real: 280s user: 277sFAIL<1>
semantics t = semantics InitGlobals_location s))
failed.
Failed to prove theorem full_make_init_semantics.
Exception raised at Thm_cont.DISCH_THEN:
(THEN1 on line 3285)
error in quse /home/myreen/regression/cakeml-1314/compiler/backend/proofs/stack_to_labProofScript.sml : HOL_ERR {message = " (THEN1 on line 3285)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
error in load /home/myreen/regression/cakeml-1314/compiler/backend/proofs/stack_to_labProofScript : HOL_ERR {message = " (THEN1 on line 3285)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
Uncaught exception: HOL_ERR {message = " (THEN1 on line 3285)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}