CakeML:cae691cf208891e454a00b158d0a41a56736114c
Update diffTheory to use mlnumTheory
#401 (Num_from_to_string)
Merging into:c760e35a371970c83a07a154bb67d4b842115a1f
Merge pull request #399 from CakeML/silent-ffi-on-gc
HOL:0d6b905d29aaa0c093e28f41dd1459514487c729
Update importer for latest version L3.
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux
Claimed job
Building HOL
Resuming semantics/ffi
Finished semantics/ffi 7m35s 390MB
Starting semantics
Finished semantics 10m16s 1GB
Starting semantics/proofs
Finished semantics/proofs 7m15s 1GB
Starting basis/pure
Finished basis/pure 6m10s 740MB
Starting translator
Finished translator 7m03s 1GB
Starting compiler/parsing
Finished compiler/parsing 4m16s 2GB
Starting characteristic
Finished characteristic 4m32s 1GB
Starting basis
Finished basis 27m58s 2GB
Starting translator/monadic
Finished translator/monadic 3m36s 1GB
Starting compiler/inference
Finished compiler/inference 2m45s 973MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 46s 813MB
Starting compiler/backend/gc
FAILED: compiler/backend/gc
]0;Holmake: ..Recursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/multiwordRecursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/multiwordStarting work on multiwordTheory
multiwordTheory OK
Starting work on mc_multiwordTheory
mc_multiwordTheory OK
Finished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/machine-code/multiword
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/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-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/examples/l3-machine-code/commonStarting work on tripleTheory
Starting work on stateTheory
tripleTheory OK
stateTheory OK
Starting work on temporal_stateTheory
temporal_stateTheory OK
Finished recursive invocation in /scratch/cakeml/regression/HOL-0d6b905d29aaa0c093e28f41dd1459514487c729/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
lab_filterTheory OK
Starting work on lab_to_targetTheory
modLangTheory OK
Starting work on conLangTheory
stackLangTheory OK
Starting work on wordLangTheory
closLangTheory OK
Starting work on bviTheory
bviTheory OK
Starting work on dataLangTheory
conLangTheory OK
Starting work on bvi_letTheory
dataLangTheory OK
Starting work on data_liveTheory
wordLangTheory OK
Starting work on data_simpTheory
bvi_letTheory OK
Starting work on data_spaceTheory
lab_to_targetTheory OK
Starting work on bvi_tailrecTheory
data_simpTheory OK
Starting work on bvlTheory
data_liveTheory OK
Starting work on clos_annotateTheory
bvlTheory OK
Starting work on bvl_constTheory
data_spaceTheory OK
Starting work on bvi_to_dataTheory
bvi_tailrecTheory OK
Starting work on bvl_jumpTheory
clos_annotateTheory OK
Starting work on clos_callTheory
bvl_jumpTheory OK
Starting work on clos_knownTheory
clos_callTheory OK
Starting work on clos_mtiTheory
bvi_to_dataTheory OK
Starting work on clos_numberTheory
clos_numberTheory OK
Starting work on con_to_decTheory
clos_mtiTheory OK
Starting work on word_bignumTheory
con_to_decTheory OK
Starting work on word_allocTheory
clos_knownTheory OK
Starting work on clos_to_bvlTheory
bvl_constTheory OK
Starting work on bvl_handleTheory
bvl_handleTheory OK
Starting work on bvl_inlineTheory
word_bignumTheory OK
Starting work on word_instTheory
bvl_inlineTheory OK
Starting work on bvl_to_bviTheory
clos_to_bvlTheory OK
Starting work on word_removeTheory
word_removeTheory OK
Starting work on word_simpTheory
word_instTheory OK
Starting work on exhLangTheory
exhLangTheory OK
Starting work on exh_reorderTheory
exh_reorderTheory OK
Starting work on dec_to_exhTheory
bvl_to_bviTheory OK
Starting work on patLangTheory
dec_to_exhTheory OK
Starting work on mod_to_conTheory
patLangTheory OK
Starting work on exh_to_patTheory
mod_to_conTheory OK
Starting work on pat_to_closTheory
word_simpTheory OK
Starting work on displayLangTheory
displayLangTheory FAILED! <1>
(num :num)
on line 27, characters 57-61
unification failure message: Attempt to unify different type operators: integer$int and num$num
error in quse /scratch/cakeml/regression/cakeml-69/compiler/backend/displayLangScript.sml : HOL_ERR {message = "on line 27, characters 57-61:\n\nType inference failure: unable to infer a type for the application of\n\nnum_to_json :int -> obj\n\non line 27, characters 45-55\n\nto\n\n(num :num)\n\non line 27, characters 57-61\n\nunification failure message: Attempt to unify different type operators: integer$int and num$num\n", origin_function = "type-analysis", origin_structure = "Preterm"}
error in load displayLangScript : HOL_ERR {message = "on line 27, characters 57-61:\n\nType inference failure: unable to infer a type for the application of\n\nnum_to_json :int -> obj\n\non line 27, characters 45-55\n\nto\n\n(num :num)\n\non line 27, characters 57-61\n\nunification failure message: Attempt to unify different type operators: integer$int and num$num\n", origin_function = "type-analysis", origin_structure = "Preterm"}
Uncaught exception: HOL_ERR {message = "on line 27, characters 57-61:\n\nType inference failure: unable to infer a type for the application of\n\nnum_to_json :int -> obj\n\non line 27, characters 45-55\n\nto\n\n(num :num)\n\non line 27, characters 57-61\n\nunification failure message: Attempt to unify different type operators: integer$int and num$num\n", origin_function = "type-analysis", origin_structure = "Preterm"}
word_allocTheory M-KILLED
exh_to_patTheory M-KILLED
pat_to_closTheory M-KILLED
Finished recursive invocation in ..
]0;Holmake: .