Job 1097

CakeML:fa186f6cfb9bfb08eaa4b872c1fecb943868b227
  Merge pull request #698 from CakeML/cakeml-rat-proj [Nov 16 15:11:37]
HOL:936859192dd87d43dd739a7f93c3695617e5bf14
  Make parsing fail if Unicode logical negation ( [Nov 17 23:49:38]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 18 23:14:46 Claimed job
Nov 18 23:14:54 Building HOL
Nov 18 23:24:30 Starting developers
Nov 18 23:24:32 Finished developers                                               1s 109MB
Nov 18 23:24:32 Starting developers/bin
Nov 18 23:24:36 Finished developers/bin                                           3s 165MB
Nov 18 23:24:36 Starting semantics/ffi
Nov 18 23:24:44 Finished semantics/ffi                                            7s 230MB
Nov 18 23:24:44 Starting semantics
Nov 18 23:26:10 Finished semantics                                             1m25s 841MB
Nov 18 23:26:10 Starting semantics/proofs
Nov 18 23:29:12 Finished semantics/proofs                                      3m01s   1GB
Nov 18 23:29:12 Starting semantics/alt_semantics
Nov 18 23:29:19 Finished semantics/alt_semantics                                  6s 294MB
Nov 18 23:29:19 Starting semantics/alt_semantics/proofs
Nov 18 23:31:09 Finished semantics/alt_semantics/proofs                        1m49s 739MB
Nov 18 23:31:09 Starting basis/pure
Nov 18 23:34:02 Finished basis/pure                                            2m52s 838MB
Nov 18 23:34:02 Starting translator
Nov 18 23:35:49 Finished translator                                            1m46s   1GB
Nov 18 23:35:49 Starting compiler/parsing
Nov 18 23:36:56 Finished compiler/parsing                                      1m06s   1GB
Nov 18 23:36:56 Starting characteristic
Nov 18 23:42:16 Finished characteristic                                        5m20s   1GB
Nov 18 23:42:17 Starting translator/monadic
Nov 18 23:43:44 Finished translator/monadic                                    1m27s   1GB
Nov 18 23:43:45 Starting basis
Nov 19 00:03:39 Finished basis                                                19m53s   2GB
Nov 19 00:03:39 Starting compiler/inference
Nov 19 00:05:24 Finished compiler/inference                                    1m44s   1GB
Nov 19 00:05:25 Starting compiler/backend/reg_alloc
Nov 19 00:06:25 Finished compiler/backend/reg_alloc                              59s   1GB
Nov 19 00:06:25 Starting compiler/backend/gc
Nov 19 00:07:00 FAILED: compiler/backend/gc
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[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$(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)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Starting work on multiwordTheory
Starting work on asmTheory
Starting work on backend_commonTheory
Starting work on README.md
README.md                                                                       real:    0s  user:    0s     OK
Starting work on gc_sharedTheory
asmTheory                                                                       real:    5s  user:    5s     OK
backend_commonTheory                                                            real:   10s  user:    9s     OK
Starting work on closLangTheory
Starting work on stackLangTheory
gc_sharedTheory                                                                 real:   14s  user:   14s     OK
Starting work on copying_gcTheory
stackLangTheory                                                                 real:    9s  user:    9s     OK
Starting work on wordLangTheory
closLangTheory                                                                  real:   11s  user:   11s     OK
Starting work on dataLangTheory
multiwordTheory                                                                 real:   27s  user:   26s     OK
Starting work on mc_multiwordTheory
copying_gcTheory                                                                real:   14s  user:   13s     OK
Starting work on gen_gcTheory
dataLangTheory                                                                  real:   10s  user:    9s     OK
wordLangTheory                                                                  real:   13s  user:   13sFAIL<1>
 
 which has type
 
 : word
 
 unification failure message: Attempt to unify different type operators: min$bool and fcp$cart
 
 error in quse /home/myreen/regression/cakeml-1097/compiler/backend/wordLangScript.sml : HOL_ERR {message = "on line 257, characters 41-42:\n\nType inference failure: unable to infer a type for the application of\n\n$~ :bool -> bool\n\nat line 257, character 40\n\nto\n\n(0w :\206\177 word)\n\non line 257, characters 41-42\n\nwhich has type\n\n:\206\177 word\n\nunification failure message: Attempt to unify different type operators: min$bool and fcp$cart\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /home/myreen/regression/cakeml-1097/compiler/backend/wordLangScript : HOL_ERR {message = "on line 257, characters 41-42:\n\nType inference failure: unable to infer a type for the application of\n\n$~ :bool -> bool\n\nat line 257, character 40\n\nto\n\n(0w :\206\177 word)\n\non line 257, characters 41-42\n\nwhich has type\n\n:\206\177 word\n\nunification failure message: Attempt to unify different type operators: min$bool and fcp$cart\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 257, characters 41-42:\n\nType inference failure: unable to infer a type for the application of\n\n$~ :bool -> bool\n\nat line 257, character 40\n\nto\n\n(0w :\206\177 word)\n\non line 257, characters 41-42\n\nwhich has type\n\n:\206\177 word\n\nunification failure message: Attempt to unify different type operators: min$bool and fcp$cart\n", origin_function = "type-analysis", origin_structure = "Preterm"}
mc_multiwordTheory                                                                                      M-KILLED
gen_gcTheory                                                                                            M-KILLED