OverviewCakeML:4545556a74fc514d40693abe6d681984170cb92f
Merge branch 'master' into fix_build_instrs
#744 (fix_build_instrs)
Merging into:c89761b7ef55823e5883bc0c3b0dd2b5291b05d4
Get some files to build again
HOL:a084f49e1bf9a108a354cd01a025118182b72fd5
emacs-mode: Fix error in detection of end of open declarations
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 134MB
Starting developers/bin
Finished developers/bin 12s 1GB
Starting semantics/ffi
Finished semantics/ffi 23s 296MB
Starting semantics
Finished semantics 4m56s 2GB
Starting semantics/proofs
Finished semantics/proofs 9m09s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 37s 429MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 8m37s 1GB
Starting basis/pure
Finished basis/pure 6m53s 1GB
Starting translator
Finished translator 5m13s 2GB
Starting compiler/parsing
Finished compiler/parsing 2m24s 2GB
Starting characteristic
Finished characteristic 8m49s 4GB
Starting translator/monadic
Finished translator/monadic 2m07s 1GB
Starting basis
Finished basis 35m40s 26GB
Starting compiler/inference
Finished compiler/inference 1m09s 2GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m08s 2GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m44s 3GB
Starting compiler/backend
Finished compiler/backend 5m17s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 22s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m01s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 1m48s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 38s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m14s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m27s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 20s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 19s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 19s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m08s 2GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 2m13s 2GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m18s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 26m52s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m20s 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 README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md real: 0s user: 0s OK
Starting work on data_simpProofTheory
reachable_sptProofTheory real: 15s user: 14s OK
Starting work on data_spaceProofTheory
data_simpProofTheory real: 18s user: 17s OK
Starting work on bvl_constProofTheory
data_spaceProofTheory real: 37s user: 35s OK
Starting work on bvi_letProofTheory
data_liveProofTheory real: 82s user: 80s OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory real: 63s user: 62s OK
Starting work on bvl_handleProofTheory
bvi_letProofTheory real: 29s user: 28s OK
Starting work on clos_annotateProofTheory
bvl_handleProofTheory real: 24s user: 23s OK
Starting work on bvl_inlineProofTheory
clos_annotateProofTheory real: 29s user: 28s OK
Starting work on clos_callProofTheory
bvl_inlineProofTheory real: 43s user: 41s OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory real: 22s user: 21s OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory real: 16s user: 15s OK
Starting work on clos_letopProofTheory
bvi_tailrecProofTheory real: 206s user: 202s OK
Starting work on bvl_to_bviProofTheory
clos_letopProofTheory real: 25s user: 23s OK
Starting work on clos_ticksProofTheory
bvi_to_dataProofTheory real: 137s user: 134s OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory real: 28s user: 27s OK
Starting work on clos_knownProofTheory
clos_mtiProofTheory real: 42s user: 39s OK
Starting work on clos_numberProofTheory
clos_numberProofTheory real: 37s user: 34s OK
Starting work on bvl_jumpProofTheory
clos_callProofTheory real: 201s user: 196s OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory real: 16s user: 15s OK
Starting work on word_bignumProofTheory
word_simpProofTheory real: 62s user: 61s OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory real: 151s user: 147s OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory real: 39s user: 38s OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory real: 214s user: 210s OK
Starting work on word_allocProofTheory
word_bignumProofTheory real: 257s user: 252s OK
Starting work on word_instProofTheory
word_instProofTheory real: 61s user: 59s OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory real: 242s user: 237s OK
Starting work on word_depthProofTheory
word_removeProofTheory real: 33s user: 31s OK
Starting work on flat_patternProofTheory
word_depthProofTheory real: 69s user: 67s OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory real: 50s user: 49s OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory real: 60s user: 58s OK
Starting work on stack_removeProofTheory
lab_filterProofTheory real: 62s user: 60s OK
Starting work on flat_elimProofTheory
flat_elimProofTheory real: 64s user: 63s OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory real: 104s user: 101s OK
Starting work on stack_allocProofTheory
word_allocProofTheory real: 570s user: 564s OK
Starting work on word_to_wordProofTheory
stack_removeProofTheory real: 249s user: 246s OK
Starting work on lab_to_targetProofTheory
word_to_wordProofTheory real: 66s user: 64s OK
Starting work on stack_namesProofTheory
stack_namesProofTheory real: 31s user: 30s OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory real: 66s user: 64s OK
Starting work on word_to_stackProofTheory
data_to_word_memoryProofTheory real: 750s user: 738s OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory real: 230s user: 227s OK
Starting work on word_elimProofTheory
word_elimProofTheory real: 121s user: 119s OK
stack_allocProofTheory real: 425s user: 418s OK
data_to_word_gcProofTheory real: 235s user: 232s OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory real: 192s user: 190s OK
Starting work on data_to_word_assignProofTheory
data_to_word_assignProofTheory real: 1026s user: 1012s OK
Starting work on data_to_wordProofTheory
word_to_stackProofTheory real: 1573s user: 1544s OK
Starting work on stack_to_labProofTheory
data_to_wordProofTheory real: 210s user: 205s OK
stack_to_labProofTheory real: 268s user: 264sFAIL<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-1315/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-1315/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"}