CakeML:2c58750b3b4f78553e1afd68f0aab42ce079d2c9
Merge remote-tracking branch 'origin/master' into readme
#566 (readme)
Merging into:1b447042a65d0ce7c62341a3592d12b1a99eb144
Fix word_elimProof for latest HOL
HOL:8649983c4924097c8a62e531247200c9bf24067c
Fix bug in lexing of strings like x'0 followed by symbolic chars
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 21MB
Starting developers/bin
Finished developers/bin 29s 140MB
Starting semantics/ffi
Finished semantics/ffi 35s 404MB
Starting semantics
Finished semantics 1m26s 847MB
Starting semantics/proofs
Finished semantics/proofs 2m50s 1GB
Starting basis/pure
Finished basis/pure 3m37s 655MB
Starting translator
Finished translator 1m11s 876MB
Starting compiler/parsing
Finished compiler/parsing 1m16s 1GB
Starting characteristic
Finished characteristic 2m29s 1GB
Starting translator/monadic
Finished translator/monadic 1m25s 1GB
Starting basis
Finished basis 16m14s 3GB
Starting compiler/inference
Finished compiler/inference 1m38s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 45s 976MB
Starting compiler/backend/gc
Finished compiler/backend/gc 7m24s 1GB
Starting compiler/backend
Finished compiler/backend 1s 18MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 17MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 48s 568MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 1m42s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 23s 534MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 57s 764MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 59s 842MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 16s 822MB
Starting compiler/backend/x64
Finished compiler/backend/x64 16s 902MB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 17s 840MB
Starting compiler/backend/mips
Finished compiler/backend/mips 16s 951MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 17s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m14s 870MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m04s 829MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m53s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 9m00s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 2m42s 552MB
Starting compiler/backend/proofs
FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/balanced_bst]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/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 $(CAKEMLDIR)/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/monad_base]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: ../../../translator/monadic/monad_base]0;Holmake: ../../../translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[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-8649983c4924097c8a62e531247200c9bf24067c/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8649983c4924097c8a62e531247200c9bf24067c/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: ../../../translator/monadic]0;Holmake: ../../../characteristic]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: ../../../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/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
Starting work on README.md
README.md OK
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
word_removeProofTheory OK
Starting work on flat_exh_matchProofTheory
flat_elimProofTheory 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
word_allocProofTheory OK
Starting work on word_to_wordProofTheory
stack_removeProofTheory OK
Starting work on lab_to_targetProofTheory
word_to_wordProofTheory FAILED! <1>
domain rst.code = domain rst1.code
rst1 =
rst with
<|code := rst1.code;
compile_oracle :=
(I ## MAP (p. compile_single tt kk aa co (p,NONE)))
rst.compile_oracle; compile := cc|>))
failed.
Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 406) (THEN1 on line 410) (THEN1 on line 421) (THEN1 on line 426) (THEN1 on line 429) (THEN1 on line 385) (THEN1 on line 220) (THEN1 on line 474) (THEN1 on line 523) (THEN1 on line 532) (THEN1 on line 547) (THEN1 on line 548) (THEN1 on line 549) (THEN1 on line 550) (THEN1 on line 551) (THEN1 on line 572) (THEN1 on line 573) (THEN1 on line 574)", origin_function = "THEN1", origin_structure = "Tactical"}
stack_allocProofTheory M-KILLED
word_to_stackProofTheory M-KILLED
lab_to_targetProofTheory M-KILLED