Job 1186

CakeML:7ce8576853919407449b6e81913dc4bd23dd426b
  Un-modify a case/dtcase [Feb 19 09:09:45]
#724 (constrain_op_case)
Merging into:ed66b67fb3e2faf1ea517dff415c277cad73c8dc
  Merge pull request #714 from CakeML/nopacklib [Feb 16 18:25:28]
HOL:bbb3ac95bcef6f8adbfbd04dae34c4d8df19de22
  Extend/improve REALMULCANON normalisation [Feb 18 05:54:10]
Machine:oven3 4.19.67.1.amd64-smp

Feb 19 11:04:32 Claimed job
Feb 19 11:04:41 Building HOL
Feb 19 11:29:30 Starting developers
Feb 19 11:29:37 Finished developers                                               6s 122MB
Feb 19 11:29:37 Starting developers/bin
Feb 19 11:29:52 Finished developers/bin                                          14s   1GB
Feb 19 11:29:52 Starting semantics/ffi
Feb 19 11:30:16 Finished semantics/ffi                                           23s 241MB
Feb 19 11:30:16 Starting semantics
Feb 19 11:33:19 Finished semantics                                             3m02s   1GB
Feb 19 11:33:19 Starting semantics/proofs
Feb 19 11:40:24 Finished semantics/proofs                                      7m04s   1GB
Feb 19 11:40:24 Starting semantics/alt_semantics
Feb 19 11:40:44 Finished semantics/alt_semantics                                 19s 330MB
Feb 19 11:40:44 Starting semantics/alt_semantics/proofs
Feb 19 11:45:04 Finished semantics/alt_semantics/proofs                        4m19s 855MB
Feb 19 11:45:04 Starting basis/pure
Feb 19 11:51:07 Finished basis/pure                                            6m03s 970MB
Feb 19 11:51:07 Starting translator
Feb 19 11:56:17 Finished translator                                            5m09s   1GB
Feb 19 11:56:17 Starting compiler/parsing
Feb 19 11:58:42 Finished compiler/parsing                                      2m24s   2GB
Feb 19 11:58:42 Starting characteristic
Feb 19 12:10:49 Finished characteristic                                       12m06s   1GB
Feb 19 12:10:49 Starting translator/monadic
Feb 19 12:14:00 Finished translator/monadic                                    3m10s   1GB
Feb 19 12:14:00 Starting basis
Feb 19 13:18:21 Finished basis                                              1h04m21s  12GB
Feb 19 13:18:21 Starting compiler/inference
Feb 19 13:20:07 FAILED: compiler/inference
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[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$(HOLDIR)/examples/machine-code/hoare-triple[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)/semantics/proofs[0m
Starting work on commonUnifTheory
Starting work on README.md
Starting work on infer_tTheory
README.md                                                                                                                                                    real:    0s  user:    0s     OK
commonUnifTheory                                                                                                                                             real:    2s  user:    1s     OK
Starting work on termTheory
termTheory                                                                                                                                                   real:    3s  user:    2s     OK
Starting work on substTheory
substTheory                                                                                                                                                  real:    5s  user:    4s     OK
Starting work on walkTheory
walkTheory                                                                                                                                                   real:    4s  user:    4s     OK
Starting work on walkstarTheory
walkstarTheory                                                                                                                                               real:    5s  user:    4s     OK
Starting work on collapseTheory
Starting work on unifDefTheory
infer_tTheory                                                                                                                                                real:   21s  user:   19s     OK
collapseTheory                                                                                                                                               real:    3s  user:    2s     OK
unifDefTheory                                                                                                                                                real:    8s  user:    8s     OK
Starting work on unifPropsTheory
unifPropsTheory                                                                                                                                              real:    7s  user:    7s     OK
Starting work on unifyTheory
unifyTheory                                                                                                                                                  real:   34s  user:   33s     OK
Starting work on inferTheory
inferTheory                                                                                                                                                  real:   30s  user:   28sFAIL<1>
 
 (top :( -> bool) # ( ->  -> bool) ->  -> bool ) :( -> bool) # ( ->  -> bool) ->  -> bool
 
 on line 419, characters 13-15
 
 unification failure message: Attempt to unify different type operators: fpSem$fp_top and min$fun
 
 error in quse /root/regression/cakeml-1186/compiler/inference/inferScript.sml : HOL_ERR {message = "on line 419, characters 13-15:\n\nType inference failure: unable to infer a type for the application of\n\nFP_top :fp_top -> op\n\non line 419, characters 6-11\n\nto\n\n(top :(\206\177 -> bool) # (\206\177 -> \206\177 -> bool) -> \206\177 -> bool ) :(\206\177 -> bool) # (\206\177 -> \206\177 -> bool) -> \206\177 -> bool\n\non line 419, characters 13-15\n\nunification failure message: Attempt to unify different type operators: fpSem$fp_top and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /root/regression/cakeml-1186/compiler/inference/inferScript : HOL_ERR {message = "on line 419, characters 13-15:\n\nType inference failure: unable to infer a type for the application of\n\nFP_top :fp_top -> op\n\non line 419, characters 6-11\n\nto\n\n(top :(\206\177 -> bool) # (\206\177 -> \206\177 -> bool) -> \206\177 -> bool ) :(\206\177 -> bool) # (\206\177 -> \206\177 -> bool) -> \206\177 -> bool\n\non line 419, characters 13-15\n\nunification failure message: Attempt to unify different type operators: fpSem$fp_top and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 419, characters 13-15:\n\nType inference failure: unable to infer a type for the application of\n\nFP_top :fp_top -> op\n\non line 419, characters 6-11\n\nto\n\n(top :(\206\177 -> bool) # (\206\177 -> \206\177 -> bool) -> \206\177 -> bool ) :(\206\177 -> bool) # (\206\177 -> \206\177 -> bool) -> \206\177 -> bool\n\non line 419, characters 13-15\n\nunification failure message: Attempt to unify different type operators: fpSem$fp_top and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}