Overview

Job 75

CakeML:cae691cf208891e454a00b158d0a41a56736114c
  Update diffTheory to use mlnumTheory
#401 (Num_from_to_string)
Merging into:b2cf5b279dc4839f3d2f09b76cda9ec902066fa2
  Add missing case for config errors
HOL:1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd
  Make sure recent new constants (from CakeML) are in compsets
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting semantics/ffi
 Finished semantics/ffi                                         1m06s 319MB
 Starting semantics
 Finished semantics                                             2m36s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m31s 966MB
 Starting basis/pure
 Finished basis/pure                                            6m15s 625MB
 Starting translator
 Finished translator                                            7m05s 907MB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m34s   2GB
 Starting characteristic
 Finished characteristic                                        4m37s   1GB
 Starting basis
 Finished basis                                                28m42s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m39s   1GB
 Starting compiler/inference
 Finished compiler/inference                                    2m50s 907MB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              48s 814MB
 Starting compiler/backend/gc
 FAILED: compiler/backend/gc
]0;Holmake: ..Recursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/multiwordRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/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-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/machine-code/multiword
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/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-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/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-1e9e2856a1cfb8567d3cba5aa2066e67a4507ecd/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
stackLangTheory                                                              OK
Starting work on wordLangTheory
lab_filterTheory                                                             OK
Starting work on lab_to_targetTheory
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
bvi_letTheory                                                                OK
Starting work on data_simpTheory
wordLangTheory                                                               OK
Starting work on data_spaceTheory
lab_to_targetTheory                                                          OK
Starting work on bvi_tailrecTheory
data_simpTheory                                                              OK
Starting work on bvlTheory
bvlTheory                                                                    OK
Starting work on bvl_constTheory
data_liveTheory                                                              OK
Starting work on bvl_jumpTheory
data_spaceTheory                                                             OK
Starting work on bvi_to_dataTheory
bvl_jumpTheory                                                               OK
Starting work on clos_annotateTheory
bvi_tailrecTheory                                                            OK
Starting work on clos_callTheory
clos_annotateTheory                                                          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
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
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-75/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: .