Overview

Job 657

CakeML:289880182b8bf5cc04dd7efcbd9c9c5025be89f7
  Bugfix in EVAL setup in ml_progLib changes.
#595 (local)
Merging into:6669d99667b1f4dbb60de32048f97f611277f41e
  Remove unused parsing gitignore
HOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748
  Fix bug: TypeBase.simpls_of not being filled in on load
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  30MB
 Starting developers/bin
 Finished developers/bin                                          34s 140MB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 217MB
 Starting semantics
 Finished semantics                                             1m21s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m24s   1GB
 Starting basis/pure
 Finished basis/pure                                              51s 923MB
 Starting translator
 Finished translator                                            1m41s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m05s   1GB
 Starting characteristic
 FAILED: characteristic
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/basis/pure]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/balanced_bst]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-657/basis/pure]0;Holmake: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/cakeml-657/developers]0;Holmake: ~/regression/cakeml-657/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/cakeml-657/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-657/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/cakeml-657/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-657/basis/pure]0;Holmake: ~/regression/cakeml-657/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/compiler/parsing]0;Holmake: ~/regression/cakeml-657/semantics]0;Holmake: ~/regression/cakeml-657/semantics/ffi]0;Holmake: ~/regression/cakeml-657/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-657/semantics]0;Holmake: ~/regression/cakeml-657/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-657/compiler/parsing]0;Holmake: ~/regression/cakeml-657/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/semantics/proofs]0;Holmake: ~/regression/cakeml-657/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/translator]0;Holmake: ~/regression/cakeml-657/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/characteristic[0m
Starting work on cfFFITypeTheory
Starting work on README.md
README.md                                           OK
cfFFITypeTheory                                     OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                                   OK
Starting work on cfHeapsTheory
cfHeapsTheory                                       OK
Starting work on cfStoreTheory
cfStoreTheory                                       OK
Starting work on cfNormaliseTheory
cfNormaliseTheory                                   OK
Starting work on cfAppTheory
cfAppTheory                                         OK
Starting work on cfTheory
cfTheory                                            OK
Starting work on cfTacticsTheory
cfTacticsTheory                                     OK
Starting work on cfLetAutoTheory
Starting work on cfMainTheory
cfMainTheory                               FAILED! <1>
 <<HOL message: Created theory "cfMain">>
 error in quse /home/myreen/regression/cakeml-657/characteristic/cfMainScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load cfMainScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
cfLetAutoTheory                               M-KILLED