Overview

Job 1191

CakeML:9f711746b20319eaaa4a25f500520ebcf26dabbf
  Fix trailing whitespace
#727 (ad-hoc-overloading)
Merging into:ed66b67fb3e2faf1ea517dff415c277cad73c8dc
  Merge pull request #714 from CakeML/nopacklib
HOL:9d20add95c75b8c69157845df5d5e74f24633371
  Merge remote-tracking branch 'origin/interaction-guide-update' into d
Machine:oven3 4.19.67.1.amd64-smp

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               7s 124MB
 Starting developers/bin
 Finished developers/bin                                          15s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           22s 261MB
 Starting semantics
 Finished semantics                                             2m37s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      7m10s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 19s 306MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        4m20s 741MB
 Starting basis/pure
 Finished basis/pure                                            1m43s 886MB
 Starting translator
 Finished translator                                            5m18s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m22s   3GB
 Starting characteristic
 Finished characteristic                                       12m10s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m12s   1GB
 Starting basis
 Finished basis                                              1h04m41s  13GB
 Starting compiler/inference
 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:   18s  user:   17s     OK
Starting work on unifyTheory
unifyTheory                                                                                                                                                  real:   34s  user:   32s     OK
Starting work on inferTheory
inferTheory                                                                                                                                                  real:   30s  user:   28sFAIL<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 /root/regression/cakeml-1191/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 /root/regression/cakeml-1191/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"}