CakeML:28567256d12006cc4e976599a0ffb82d457f98fc
Prove cheat in lab_to_targetProof
#497 (labs_exist)
Merging into:b289303609aa9526ba291ecba92f558f8f506000
Replace polyc call with $(POLYC)
HOL:7ed3f12092db2062b6fccb60e9735143ecd5c7e5
Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 8s 224MB
Starting semantics/ffi
Finished semantics/ffi 1m00s 278MB
Starting semantics
Finished semantics 2m22s 890MB
Starting semantics/proofs
Finished semantics/proofs 3m09s 1GB
Starting basis/pure
Finished basis/pure 5m47s 767MB
Starting translator
Finished translator 6m37s 974MB
Starting compiler/parsing
Finished compiler/parsing 2m10s 2GB
Starting characteristic
Finished characteristic 4m24s 1GB
Starting basis
Finished basis 28m48s 3GB
Starting translator/monadic
Finished translator/monadic 2s 13MB
Starting compiler/inference
Finished compiler/inference 2m38s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 55s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 14m54s 3GB
Starting compiler/backend
Finished compiler/backend 3s 14MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m26s 504MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 2m59s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 43s 399MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m33s 667MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m32s 697MB
Starting compiler/backend/x64
Finished compiler/backend/x64 32s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 36s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 33s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 32s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 32s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 3m56s 973MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 3m52s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 18m28s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m24s 461MB
Starting compiler/backend/proofs
FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]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/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-7ed3f12092db2062b6fccb60e9735143ecd5c7e5/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/proofs
Starting work on heap
heap OK
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
Starting work on bvi_letProofTheory
data_simpProofTheory OK
Starting work on bvi_tailrecProofTheory
data_spaceProofTheory OK
Starting work on bvl_constProofTheory
bvi_letProofTheory OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory 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_knownPropsTheory
clos_knownPropsTheory OK
Starting work on clos_knownProofTheory
bvl_inlineProofTheory OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory OK
Starting work on clos_numberProofTheory
clos_numberProofTheory OK
Starting work on con_to_decProofTheory
con_to_decProofTheory OK
Starting work on word_simpProofTheory
clos_knownProofTheory CHEATED
Starting work on word_bignumProofTheory
bvi_tailrecProofTheory OK
Starting work on bvl_to_bviProofTheory
word_simpProofTheory OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory CHEATED
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory OK
Starting work on word_allocProofTheory
word_bignumProofTheory OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory CHEATED
Starting work on word_removeProofTheory
word_instProofTheory OK
Starting work on exh_reorderProofTheory
word_removeProofTheory OK
Starting work on exh_to_patProofTheory
exh_reorderProofTheory OK
Starting work on dec_to_exhProofTheory
dec_to_exhProofTheory OK
Starting work on lab_filterProofTheory
data_to_word_memoryProofTheory OK
Starting work on stack_removeProofTheory
exh_to_patProofTheory OK
Starting work on mod_to_conProofTheory
lab_filterProofTheory OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory OK
Starting work on source_to_modProofTheory
source_to_modProofTheory OK
Starting work on stack_allocProofTheory
mod_to_conProofTheory OK
Starting work on stack_namesProofTheory
stack_removeProofTheory OK
Starting work on lab_to_targetProofTheory
stack_namesProofTheory OK
Starting work on word_to_stackProofTheory
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 clos_letopProofTheory
clos_letopProofTheory OK
Starting work on clos_ticksProofTheory
clos_ticksProofTheory OK
data_to_word_gcProofTheory OK
Starting work on data_to_word_bignumProofTheory
stack_allocProofTheory OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory FAILED! <1>
error in load stack_to_labProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 110)", origin_function = "THEN1", origin_structure = "Tactical"}
Proof of
e n q pc.
code_installed pc (append (FST (flatten e n q))) c
(l1,l2) get_labels e
v. loc_to_pc l1 l2 c = SOME v
failed.
Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 110)", origin_function = "THEN1", origin_structure = "Tactical"}
word_to_stackProofTheory M-KILLED
data_to_word_bignumProofTheory M-KILLED