CakeML Regression Test

Job 168

CakeML:2ed5cf5581874a110a2e0360cd03b9f3e877b684
  Update ml_hol_init for 'ffi type; also tidy up a bit [Jan 21 09:30:19]
#439 (monad-cleanup)
Merging into:f8dd05aea6320bbd612745b9edc67b48646124a3
  Update diffTheory to use mlnumTheory [Jan 19 16:44:16]
HOL:a061a8d27a88af555eb42dd1030099a4ecedea45
  Fixes to build logic/ltl/concrGBArepScript.sml on --expk [Jan 21 06:00:31]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Jan 21 10:24:40 Claimed job
Jan 21 10:24:49 Building HOL
Jan 21 10:37:18 Starting semantics/ffi
Jan 21 10:38:28 Finished semantics/ffi                                         1m08s 384MB
Jan 21 10:38:30 Starting semantics
Jan 21 10:41:08 Finished semantics                                             2m36s   1GB
Jan 21 10:41:10 Starting semantics/proofs
Jan 21 10:44:43 Finished semantics/proofs                                      3m29s   1GB
Jan 21 10:44:45 Starting basis/pure
Jan 21 10:50:56 Finished basis/pure                                            6m09s 678MB
Jan 21 10:50:58 Starting translator
Jan 21 10:57:55 Finished translator                                            6m55s   1GB
Jan 21 10:57:57 Starting compiler/parsing
Jan 21 11:00:22 Finished compiler/parsing                                      2m23s   1GB
Jan 21 11:00:24 Starting characteristic
Jan 21 11:05:04 Finished characteristic                                        4m38s   2GB
Jan 21 11:05:06 Starting basis
Jan 21 11:35:36 Finished basis                                                30m27s   3GB
Jan 21 11:35:38 Starting translator/monadic
Jan 21 11:39:04 Finished translator/monadic                                    3m24s   1GB
Jan 21 11:39:06 Starting compiler/inference
Jan 21 11:41:57 Finished compiler/inference                                    2m49s   1GB
Jan 21 11:41:59 Starting compiler/backend/reg_alloc
Jan 21 11:42:48 FAILED: compiler/backend/reg_alloc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-triple
]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_stubRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-free
]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: .Recursively calling Holmake in ../../../translator/monadic
]0;Holmake: ../../../translator/monadicRecursively calling Holmake in ../../../characteristic
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../compiler/parsing
]0;Holmake: ../../../compiler/parsingRecursively 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: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingFinished recursive invocation in ../../../compiler/parsing
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsFinished recursive invocation in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsFinished recursive invocation in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../translator
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorFinished recursive invocation in ../../../translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicFinished recursive invocation in ../../../characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic
]0;Holmake: .Recursively calling Holmake in ../../../unverified/reg_alloc
]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on parmoveTheory
Starting work on reg_allocTheory
parmoveTheory                                                                OK
reg_allocTheory                                                     FAILED! <1>
 Saved definition __ "extract_color_def"
 Saved definition __ "pri_move_insert_def"
 Saved definition __ "undir_move_insert_def"
 
 Exception raised at Preterm.type-analysis:
 in unknown location:
 Attempt to unify different type operators: pair$prod and num$num
 error in quse /scratch/cakeml/regression/cakeml-168/compiler/backend/reg_alloc/reg_allocScript.sml : HOL_ERR {message = "in unknown location:\nAttempt to unify different type operators: pair$prod and num$num", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load reg_allocScript : HOL_ERR {message = "in unknown location:\nAttempt to unify different type operators: pair$prod and num$num", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "in unknown location:\nAttempt to unify different type operators: pair$prod and num$num", origin_function = "type-analysis", origin_structure = "Preterm"}