CakeML:dd0443ff61629080336694113a658099938d9c7a
Update diffTheory to use mlnumTheory
#401 (Num_from_to_string)
Merging into:fadd4308da623b611c38226a5fdd50b12606080e
Add coalescing info to oracle allocator
HOL:8b5efb58d9adfab04271cef782a410e2506aa90d
Fix TeX p/printing bug caused by having multiple types of same name
Machine:cakeml1852 4.4.0-22-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting semantics/ffi
Finished semantics/ffi 19s 224MB
Starting semantics
Finished semantics 2m21s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m41s 1GB
Starting basis/pure
Finished basis/pure 1m27s 720MB
Starting translator
Finished translator 7m27s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m31s 1GB
Starting characteristic
Finished characteristic 5m05s 1GB
Starting basis
Finished basis 29m51s 2GB
Starting translator/monadic
Finished translator/monadic 3m42s 1GB
Starting compiler/inference
Finished compiler/inference 2m16s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 50s 774MB
Starting compiler/backend/gc
FAILED: compiler/backend/gc
]0;Holmake: ..Recursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/multiwordRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/machine-code/multiword
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../developers
]0;Holmake: ../../../developers]0;Holmake: ../../../developersFinished recursive invocation in ../../../developers
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubFinished recursive invocation in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscFinished recursive invocation in ../../../misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ..Recursively calling Holmake in ../reg_alloc
]0;Holmake: ../reg_allocRecursively calling Holmake in ../../../unverified/reg_alloc
]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocFinished recursive invocation in ../reg_alloc
]0;Holmake: ..Recursively calling Holmake in ../../encoders
]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders
]0;Holmake: ..Recursively calling Holmake in ../../encoders/asm
]0;Holmake: ../../encoders/asmRecursively calling Holmake in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-8b5efb58d9adfab04271cef782a410e2506aa90d/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asmRecursively calling Holmake in ../../../semantics
]0;Holmake: ../../../semanticsRecursively calling Holmake in ../../../semantics/ffi
]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiFinished recursive invocation in ../../../semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsFinished recursive invocation in ../../../semantics
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmStarting work on asmTheory
asmTheory OK
Starting work on asmSemTheory
asmSemTheory OK
Starting work on asmPropsTheory
asmPropsTheory OK
Finished recursive invocation in ../../encoders/asm
]0;Holmake: ..]0;Holmake: ..Starting work on heap
heap OK
Starting work on backend_commonTheory
Starting work on db_varsTheory
Starting work on decLangTheory
Starting work on jsonLangTheory
decLangTheory OK
Starting work on labLangTheory
backend_commonTheory OK
Starting work on closLangTheory
jsonLangTheory OK
Starting work on modLangTheory
db_varsTheory OK
Starting work on stackLangTheory
labLangTheory OK
Starting work on lab_filterTheory
modLangTheory OK
Starting work on conLangTheory
closLangTheory OK
Starting work on bviTheory
lab_filterTheory OK
Starting work on dataLangTheory
stackLangTheory OK
Starting work on bvlTheory
bviTheory OK
Starting work on bvi_letTheory
conLangTheory OK
Starting work on bvi_tailrecTheory
dataLangTheory OK
Starting work on data_liveTheory
bvlTheory OK
Starting work on data_simpTheory
data_simpTheory OK
Starting work on data_spaceTheory
bvi_letTheory OK
Starting work on bvl_constTheory
data_liveTheory OK
Starting work on bvl_jumpTheory
bvi_tailrecTheory OK
Starting work on clos_annotateTheory
bvl_jumpTheory OK
Starting work on clos_callTheory
data_spaceTheory OK
Starting work on bvi_to_dataTheory
clos_annotateTheory OK
Starting work on clos_knownTheory
clos_callTheory OK
Starting work on clos_mtiTheory
clos_mtiTheory OK
Starting work on clos_numberTheory
bvi_to_dataTheory OK
Starting work on con_to_decTheory
clos_numberTheory OK
Starting work on wordLangTheory
con_to_decTheory OK
Starting work on exhLangTheory
exhLangTheory OK
Starting work on exh_reorderTheory
wordLangTheory OK
Starting work on word_bignumTheory
exh_reorderTheory OK
Starting work on word_allocTheory
bvl_constTheory OK
Starting work on bvl_handleTheory
clos_knownTheory OK
Starting work on clos_to_bvlTheory
bvl_handleTheory OK
Starting work on bvl_inlineTheory
bvl_inlineTheory OK
Starting work on bvl_to_bviTheory
clos_to_bvlTheory OK
Starting work on word_instTheory
word_bignumTheory OK
Starting work on word_removeTheory
word_removeTheory OK
Starting work on word_simpTheory
bvl_to_bviTheory OK
word_instTheory OK
Starting work on dec_to_exhTheory
Starting work on patLangTheory
patLangTheory OK
Starting work on exh_to_patTheory
dec_to_exhTheory OK
Starting work on lab_to_targetTheory
word_simpTheory OK
Starting work on mod_to_conTheory
lab_to_targetTheory OK
Starting work on pat_to_closTheory
exh_to_patTheory OK
Starting work on displayLangTheory
mod_to_conTheory OK
Starting work on source_to_modTheory
displayLangTheory FAILED! <1>
Saved theorem _____ "sExp_Axiom"
Saved theorem _____ "sExp_induction"
<<HOL message: Defined type: "sExp">>
Exception raised at Preterm.type-analysis:
on line 23, characters 35-42:
Couldn't infer type for overloaded name toString
error in quse /scratch/cakeml/regression/cakeml-79/compiler/backend/displayLangScript.sml : HOL_ERR {message = "on line 23, characters 35-42:\nCouldn't infer type for overloaded name toString", origin_function = "type-analysis", origin_structure = "Preterm"}
error in load displayLangScript : HOL_ERR {message = "on line 23, characters 35-42:\nCouldn't infer type for overloaded name toString", origin_function = "type-analysis", origin_structure = "Preterm"}
Uncaught exception: HOL_ERR {message = "on line 23, characters 35-42:\nCouldn't infer type for overloaded name toString", origin_function = "type-analysis", origin_structure = "Preterm"}
word_allocTheory M-KILLED
pat_to_closTheory M-KILLED
source_to_modTheory M-KILLED
Finished recursive invocation in ..
]0;Holmake: .