CakeML:306e73e0ef0314393ecdbb996b50cf799375f15d
Use Git's -C option
HOL:2a42da875092fdec35e1cd69454995735c890117
Merge pull request #590 from binghe/PSL.fix
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 36s 912MB
Starting semantics/ffi
Finished semantics/ffi 38s 390MB
Starting semantics
Finished semantics 1m23s 904MB
Starting semantics/proofs
Finished semantics/proofs 2m40s 1GB
Starting basis/pure
Finished basis/pure 3m33s 631MB
Starting translator
Finished translator 1m06s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m35s 2GB
Starting characteristic
Finished characteristic 2m26s 1GB
Starting translator/monadic
Finished translator/monadic 1m24s 1GB
Starting basis
Finished basis 16m24s 3GB
Starting compiler/inference
Finished compiler/inference 1m41s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 47s 921MB
Starting compiler/backend/gc
Finished compiler/backend/gc 8m46s 3GB
Starting compiler/backend
Finished compiler/backend 2s 14MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 1s 14MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 52s 593MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 1m46s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 26s 476MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 57s 874MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m01s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 18s 1GB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 18s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 17s 919MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m10s 777MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m49s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 8m53s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m16s 571MB
Starting compiler/backend/proofs
FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/multiword]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/balanced_bst]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/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 ../../../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]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]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: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]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]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_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/l3-machine-code/common]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/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: ../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
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 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
word_bignumProofTheory OK
Starting work on word_allocProofTheory
bvl_to_bviProofTheory OK
Starting work on word_instProofTheory
word_instProofTheory OK
Starting work on word_removeProofTheory
word_removeProofTheory OK
Starting work on flat_to_patProofTheory
clos_to_bvlProofTheory CHEATED
Starting work on lab_filterProofTheory
lab_filterProofTheory OK
Starting work on stack_removeProofTheory
word_allocProofTheory FAILED! <1>
error in load word_allocProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 3988) (THEN1 on line 4016) (THEN1 on line 4019) (THEN1 on line 4022) (THEN1 on line 4035) (THEN1 on line 4039)", origin_function = "THEN1", origin_structure = "Tactical"}
Proof of
prog ssa na prog' ssa' na'.
ssa_cc_trans prog ssa na = (prog',ssa',na') ssa_map_ok na ssa
is_alloc_var na
na na' is_alloc_var na' ssa_map_ok na' ssa'
failed.
Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 3988) (THEN1 on line 4016) (THEN1 on line 4019) (THEN1 on line 4022) (THEN1 on line 4035) (THEN1 on line 4039)", origin_function = "THEN1", origin_structure = "Tactical"}
data_to_word_memoryProofTheory M-KILLED
flat_to_patProofTheory M-KILLED
stack_removeProofTheory M-KILLED