Job 1098

CakeML:7527b7e13d64c1f338c374d4eebfdeadf44c943f
  Merge pull request #706 from CakeML/parserprog-fix [Nov 20 18:22:00]
HOL:936859192dd87d43dd739a7f93c3695617e5bf14
  Make parsing fail if Unicode logical negation ( [Nov 17 23:49:38]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 20 18:41:13 Claimed job
Nov 20 18:41:20 Building HOL
Nov 20 18:52:10 Starting developers
Nov 20 18:52:14 Finished developers                                               3s  94MB
Nov 20 18:52:14 Starting developers/bin
Nov 20 18:52:21 Finished developers/bin                                           6s 960MB
Nov 20 18:52:21 Starting semantics/ffi
Nov 20 18:52:31 Finished semantics/ffi                                            9s 209MB
Nov 20 18:52:31 Starting semantics
Nov 20 18:53:57 Finished semantics                                             1m26s   1GB
Nov 20 18:53:58 Starting semantics/proofs
Nov 20 18:56:58 Finished semantics/proofs                                      3m00s   1GB
Nov 20 18:56:59 Starting semantics/alt_semantics
Nov 20 18:57:06 Finished semantics/alt_semantics                                  7s 284MB
Nov 20 18:57:06 Starting semantics/alt_semantics/proofs
Nov 20 18:58:53 Finished semantics/alt_semantics/proofs                        1m47s 966MB
Nov 20 18:58:54 Starting basis/pure
Nov 20 19:01:44 Finished basis/pure                                            2m50s 890MB
Nov 20 19:01:44 Starting translator
Nov 20 19:03:31 Finished translator                                            1m47s   1GB
Nov 20 19:03:32 Starting compiler/parsing
Nov 20 19:04:37 Finished compiler/parsing                                      1m05s   2GB
Nov 20 19:04:37 Starting characteristic
Nov 20 19:09:53 Finished characteristic                                        5m14s   1GB
Nov 20 19:09:53 Starting translator/monadic
Nov 20 19:11:21 Finished translator/monadic                                    1m27s   1GB
Nov 20 19:11:21 Starting basis
Nov 20 19:30:53 Finished basis                                                19m31s   2GB
Nov 20 19:30:53 Starting compiler/inference
Nov 20 19:32:39 Finished compiler/inference                                    1m46s   1GB
Nov 20 19:32:40 Starting compiler/backend/reg_alloc
Nov 20 19:33:39 Finished compiler/backend/reg_alloc                              59s   1GB
Nov 20 19:33:39 Starting compiler/backend/gc
Nov 20 19:34:15 FAILED: compiler/backend/gc
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
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:    4s     OK
backend_commonTheory                            real:   10s  user:    9s     OK
Starting work on closLangTheory
Starting work on stackLangTheory
gc_sharedTheory                                 real:   14s  user:   13s     OK
Starting work on copying_gcTheory
stackLangTheory                                 real:   10s  user:    9s     OK
Starting work on wordLangTheory
closLangTheory                                  real:   11s  user:   10s     OK
Starting work on dataLangTheory
multiwordTheory                                 real:   26s  user:   25s     OK
Starting work on mc_multiwordTheory
copying_gcTheory                                real:   13s  user:   12s     OK
Starting work on gen_gcTheory
dataLangTheory                                  real:   10s  user:    9s     OK
wordLangTheory                                  real:   13s  user:   12sFAIL<1>
 
 which has type
 
 : word
 
 unification failure message: Attempt to unify different type operators: min$bool and fcp$cart
 
 error in quse /home/cake/oven/regression/cakeml-1098/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/cake/oven/regression/cakeml-1098/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