Job 414

CakeML:28a1ff1087dc55d39f7a00f475bb9f812be0f522
  Fix primSemEnv for type annotations [Aug 08 18:44:15]
#509 (lem-updates)
Merging into:1802ff5409009d31ba5fe8636638bb5fc9c724df
  Fix proof in inferProg [Aug 08 13:46:34]
HOL:f243fe78da5dcc426046ce1b6a0f756e6aa524b9
  Hide vim scratch buffer from the list of buffers [Aug 08 03:52:48]
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux

Aug 08 19:02:04 Claimed job
Aug 08 19:02:13 Reusing HOL
Aug 08 19:02:31 Starting developers/bin
Aug 08 19:02:41 Finished developers/bin                                           8s 224MB
Aug 08 19:02:43 Starting semantics/ffi
Aug 08 19:03:04 Finished semantics/ffi                                           18s 260MB
Aug 08 19:03:06 Starting semantics
Aug 08 19:05:07 Finished semantics                                             1m58s 841MB
Aug 08 19:05:09 Starting semantics/proofs
Aug 08 19:10:26 Finished semantics/proofs                                      5m15s   1GB
Aug 08 19:10:28 Starting basis/pure
Aug 08 19:12:02 Finished basis/pure                                            1m31s 727MB
Aug 08 19:12:04 Starting translator
Aug 08 19:13:04 FAILED: translator
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developers[1mWorking in ../developers[0m
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../misc]0;Holmake: ../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator[0m
Starting work on heap
heap                                                                                                                                                      OK
Starting work on ml_progTheory
ml_progTheory                                                                                                                                             OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                              FAILED! <1>
 :(tvarN,  # ) alist -> ( # ) option
 
 to
 
 (funs :(,  # ) alist)
 
 on line 2048, characters 40-50
 
 unification failure message: Attempt to unify fixed variable type 'a with operator list$list
 Uncaught exception: HOL_ERR {message = "on line 2048, characters 40-50:\n\nType inference failure: unable to infer a type for the application of\n\n(find_recfun (name :tvarN) :(tvarN, \206\177 # \206\178) alist -> (\206\177 # \206\178) option)\n\non line 2048, characters 22-63\n\nwhich has type\n\n:(tvarN, \206\177 # \206\178) alist -> (\206\177 # \206\178) option\n\nto\n\n(funs :(\206\177, \206\178 # \206\179) alist)\n\non line 2048, characters 40-50\n\nunification failure message: Attempt to unify fixed variable type 'a with operator list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}