OverviewCakeML:df30bf50b46fc366b9af4840506b199138767565
Retire 'top' as a variable name
#724 (constrain_op_case)
Merging into:ed66b67fb3e2faf1ea517dff415c277cad73c8dc
Merge pull request #714 from CakeML/nopacklib
HOL:9d20add95c75b8c69157845df5d5e74f24633371
Merge remote-tracking branch 'origin/interaction-guide-update' into d
Machine:oven3 4.19.67.1.amd64-smp
Claimed job
Reusing HOL
Starting developers
Finished developers 6s 135MB
Starting developers/bin
Finished developers/bin 15s 1GB
Starting semantics/ffi
Finished semantics/ffi 23s 249MB
Starting semantics
Finished semantics 2m41s 1GB
Starting semantics/proofs
Finished semantics/proofs 6m53s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 19s 309MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 4m17s 1GB
Starting basis/pure
Finished basis/pure 1m42s 743MB
Starting translator
Finished translator 5m13s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m15s 3GB
Starting characteristic
Finished characteristic 12m03s 1GB
Starting translator/monadic
Finished translator/monadic 3m13s 1GB
Starting basis
Finished basis 1h05m20s 13GB
Starting compiler/inference
Finished compiler/inference 2m05s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m52s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 6m18s 2GB
Starting compiler/backend
Finished compiler/backend 8m15s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 45s 861MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 2m06s 994MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 3m41s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 1m11s 619MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 2m26s 980MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 2m50s 781MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 36s 760MB
Starting compiler/backend/x64
Finished compiler/backend/x64 36s 918MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 39s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 39s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 41s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 38s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 2m22s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 11m59s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 5m07s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 55m09s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m11s 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: 2s user: 2s OK
Starting work on data_simpProofTheory
reachable_sptProofTheory real: 24s user: 23s OK
Starting work on data_spaceProofTheory
data_simpProofTheory real: 28s user: 26s OK
Starting work on bvl_constProofTheory
data_spaceProofTheory real: 49s user: 46s OK
Starting work on bvi_letProofTheory
bvi_letProofTheory real: 34s user: 32s OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory real: 95s user: 92s OK
Starting work on bvl_handleProofTheory
data_liveProofTheory real: 133s user: 128s OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory real: 49s user: 46s OK
Starting work on clos_callProofTheory
bvl_handleProofTheory real: 35s user: 33s OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory real: 59s user: 56s OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory real: 30s user: 28s OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory real: 18s user: 16s OK
Starting work on clos_letopProofTheory
clos_letopProofTheory real: 33s user: 31s OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory real: 337s user: 328s OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory real: 43s user: 41s OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory real: 242s user: 236s OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory real: 59s user: 57s OK
Starting work on clos_numberProofTheory
clos_numberProofTheory real: 45s user: 43s OK
Starting work on bvl_jumpProofTheory
clos_callProofTheory real: 325s user: 317s OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory real: 19s user: 17s OK
Starting work on word_bignumProofTheory
word_simpProofTheory real: 100s user: 96s OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory real: 235s user: 229s OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory real: 46s user: 44s OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory real: 360s user: 347s OK
Starting work on word_allocProofTheory
word_bignumProofTheory real: 382s user: 370s OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory real: 376s user: 365s OK
Starting work on word_removeProofTheory
word_instProofTheory real: 89s user: 86s OK
Starting work on word_depthProofTheory
word_removeProofTheory real: 51s user: 49s OK
Starting work on flat_patternProofTheory
word_depthProofTheory real: 123s user: 119s OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory real: 86s user: 83s OK
Starting work on lab_filterProofTheory
lab_filterProofTheory real: 106s user: 102s OK
Starting work on stack_removeProofTheory
flat_to_closProofTheory real: 112s user: 108s OK
Starting work on flat_elimProofTheory
flat_elimProofTheory real: 126s user: 123s OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory real: 192s user: 187s OK
Starting work on stack_allocProofTheory
stack_removeProofTheory real: 474s user: 464s OK
Starting work on lab_to_targetProofTheory
data_to_word_memoryProofTheory real: 1175s user: 1159s OK
Starting work on stack_namesProofTheory
word_allocProofTheory real: 1122s user: 1100s OK
Starting work on word_to_wordProofTheory
stack_namesProofTheory real: 57s user: 54s OK
Starting work on stack_rawcallProofTheory
word_to_wordProofTheory real: 117s user: 114s OK
Starting work on data_to_word_gcProofTheory
stack_rawcallProofTheory real: 125s user: 122s OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory real: 413s user: 403s OK
Starting work on word_elimProofTheory
stack_allocProofTheory real: 761s user: 748s OK
word_elimProofTheory real: 229s user: 225s OK
data_to_word_gcProofTheory real: 431s user: 420s OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory real: 485s user: 478s OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory real: 2979s user: 2914s OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory real: 190s user: 183sFAIL<1>
Saved definition __ "halt_view_def"
Saved induction ___ "halt_view_ind"
Saved theorem _____ "next_lab_non_zero"
Saved theorem _____ "stack_to_lab_lab_pres"
Saved theorem _____ "stack_to_lab_lab_pres_T"
Saved theorem _____ "flatten_T_F"
Saved theorem _____ "prog_to_section_labels_ok"
error in quse /root/regression/cakeml-1188/compiler/backend/proofs/stack_to_labProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
error in load /root/regression/cakeml-1188/compiler/backend/proofs/stack_to_labProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
data_to_word_assignProofTheory M-KILLED