Job 1189

CakeML:ed66b67fb3e2faf1ea517dff415c277cad73c8dc
  Merge pull request #714 from CakeML/nopacklib [Feb 16 18:25:28]
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 20 16:17:34 Claimed job
Feb 20 16:17:37 Building HOL
Feb 20 16:29:20 Starting developers
Feb 20 16:29:24 Finished developers                                               4s 138MB
Feb 20 16:29:24 Starting developers/bin
Feb 20 16:29:31 Finished developers/bin                                           7s   1GB
Feb 20 16:29:31 Starting semantics/ffi
Feb 20 16:29:41 Finished semantics/ffi                                           10s 252MB
Feb 20 16:29:41 Starting semantics
Feb 20 16:31:07 Finished semantics                                             1m25s   1GB
Feb 20 16:31:07 Starting semantics/proofs
Feb 20 16:34:17 Finished semantics/proofs                                      3m10s 954MB
Feb 20 16:34:17 Starting semantics/alt_semantics
Feb 20 16:34:25 Finished semantics/alt_semantics                                  7s 316MB
Feb 20 16:34:25 Starting semantics/alt_semantics/proofs
Feb 20 16:36:27 Finished semantics/alt_semantics/proofs                        2m01s 760MB
Feb 20 16:36:27 Starting basis/pure
Feb 20 16:39:16 Finished basis/pure                                            2m49s 898MB
Feb 20 16:39:16 Starting translator
Feb 20 16:41:41 Finished translator                                            2m24s   1GB
Feb 20 16:41:41 Starting compiler/parsing
Feb 20 16:42:46 Finished compiler/parsing                                      1m05s   1GB
Feb 20 16:42:46 Starting characteristic
Feb 20 16:48:26 Finished characteristic                                        5m39s   1GB
Feb 20 16:48:26 Starting translator/monadic
Feb 20 16:49:59 Finished translator/monadic                                    1m32s   1GB
Feb 20 16:49:59 Starting basis
Feb 20 17:19:52 Finished basis                                                29m53s  20GB
Feb 20 17:19:52 Starting compiler/inference
Feb 20 17:20:41 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:    1s  user:    0s     OK
Starting work on termTheory
termTheory                                      real:    1s  user:    1s     OK
Starting work on substTheory
substTheory                                     real:    2s  user:    2s     OK
Starting work on walkTheory
walkTheory                                      real:    2s  user:    1s     OK
Starting work on walkstarTheory
infer_tTheory                                   real:    9s  user:    8s     OK
walkstarTheory                                  real:    2s  user:    1s     OK
Starting work on collapseTheory
Starting work on unifDefTheory
collapseTheory                                  real:    1s  user:    0s     OK
unifDefTheory                                   real:    3s  user:    3s     OK
Starting work on unifPropsTheory
unifPropsTheory                                 real:    3s  user:    2s     OK
Starting work on unifyTheory
unifyTheory                                     real:   16s  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-1189/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-1189/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"}