Job 1192

CakeML:210f5c2ce0804027acbac59d87eab48cdeed1625
  Merge pull request #727 from IlmariReissumies/ad-hoc-overloading [Feb 21 09:48:53]
HOL:9d20add95c75b8c69157845df5d5e74f24633371
  Merge remote-tracking branch 'origin/interaction-guide-update' into d [Feb 19 09:30:56]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Feb 21 10:01:55 Claimed job
Feb 21 10:01:59 Reusing HOL
Feb 21 10:02:43 Starting developers
Feb 21 10:02:48 Finished developers                                               4s 124MB
Feb 21 10:02:48 Starting developers/bin
Feb 21 10:02:55 Finished developers/bin                                           6s   1GB
Feb 21 10:02:55 Starting semantics/ffi
Feb 21 10:03:05 Finished semantics/ffi                                            9s 238MB
Feb 21 10:03:05 Starting semantics
Feb 21 10:04:22 Finished semantics                                             1m16s   1GB
Feb 21 10:04:22 Starting semantics/proofs
Feb 21 10:07:29 Finished semantics/proofs                                      3m06s   1GB
Feb 21 10:07:29 Starting semantics/alt_semantics
Feb 21 10:07:37 Finished semantics/alt_semantics                                  7s 332MB
Feb 21 10:07:37 Starting semantics/alt_semantics/proofs
Feb 21 10:09:36 Finished semantics/alt_semantics/proofs                        1m59s 764MB
Feb 21 10:09:36 Starting basis/pure
Feb 21 10:10:24 Finished basis/pure                                              47s 711MB
Feb 21 10:10:24 Starting translator
Feb 21 10:12:51 Finished translator                                            2m26s   1GB
Feb 21 10:12:51 Starting compiler/parsing
Feb 21 10:13:55 Finished compiler/parsing                                      1m04s   1GB
Feb 21 10:13:56 Starting characteristic
Feb 21 10:19:35 Finished characteristic                                        5m38s   2GB
Feb 21 10:19:35 Starting translator/monadic
Feb 21 10:21:07 Finished translator/monadic                                    1m31s   1GB
Feb 21 10:21:07 Starting basis
Feb 21 10:51:17 Finished basis                                                30m08s   9GB
Feb 21 10:51:17 Starting compiler/inference
Feb 21 10:51:58 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 README.md
Starting work on infer_tTheory
README.md                                       real:    0s  user:    0s     OK
infer_tTheory                                   real:    9s  user:    8s     OK
Starting work on unifyTheory
unifyTheory                                     real:   15s  user:   15s     OK
Starting work on inferTheory
inferTheory                                     real:   15s  user:   13sFAIL<1>
 
 (top :( -> bool) # ( ->  -> bool) ->  -> bool ) :( -> bool) # ( ->  -> bool) ->  -> bool
 
 on line 429, characters 13-15
 
 unification failure message: Attempt to unify different type operators: fpSem$fp_top and min$fun
 
 error in quse /home/cur/sao/cakeml/regression/cakeml-1192/compiler/inference/inferScript.sml : HOL_ERR {message = "on line 429, 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 429, 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 429, 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 /home/cur/sao/cakeml/regression/cakeml-1192/compiler/inference/inferScript : HOL_ERR {message = "on line 429, 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 429, 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 429, 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 429, 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 429, 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 429, 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"}