Job 920

CakeML:55bcf9b13e7e80741070b122b1d8599effddd232
  Change definition of cause_type_error [Jun 28 15:58:04]
#661 (divord)
Merging into:5cd3c1dad6a712dd528d4717fe43410444eeeff2
  Merge pull request #660 from Gaj7/master [Jun 19 16:55:24]
HOL:27b999029af7e69c3496b29a745728c30561192b
  Fix regular-play/selftest.sml given testutils changes [Jun 26 01:16:59]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 28 19:09:22 Claimed job
Jun 28 19:09:28 Building HOL
Jun 28 19:17:16 Starting developers
Jun 28 19:17:17 Finished developers                                               0s  20MB
Jun 28 19:17:17 Starting developers/bin
Jun 28 19:17:21 Finished developers/bin                                           2s 144MB
Jun 28 19:17:21 Starting semantics/ffi
Jun 28 19:17:54 Finished semantics/ffi                                           32s 494MB
Jun 28 19:17:54 Starting semantics
Jun 28 19:19:22 Finished semantics                                             1m28s   1GB
Jun 28 19:19:23 Starting semantics/proofs
Jun 28 19:22:24 Finished semantics/proofs                                      3m01s   1GB
Jun 28 19:22:25 Starting semantics/alt_semantics
Jun 28 19:22:31 Finished semantics/alt_semantics                                  5s 262MB
Jun 28 19:22:31 Starting semantics/alt_semantics/proofs
Jun 28 19:24:19 Finished semantics/alt_semantics/proofs                        1m47s 679MB
Jun 28 19:24:19 Starting basis/pure
Jun 28 19:27:52 Finished basis/pure                                            3m32s 704MB
Jun 28 19:27:52 Starting translator
Jun 28 19:29:30 Finished translator                                            1m37s   1GB
Jun 28 19:29:30 Starting compiler/parsing
Jun 28 19:30:10 FAILED: compiler/parsing
]0;Holmake: .]0;Holmake: ~/regression/cakeml-920/misc]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-920/misc]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-920/misc]0;Holmake: ~/regression/cakeml-920/developers]0;Holmake: ~/regression/cakeml-920/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-920/misc]0;Holmake: ~/regression/cakeml-920/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-920/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-920/misc]0;Holmake: ~/regression/cakeml-920/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-920/semantics]0;Holmake: ~/regression/cakeml-920/semantics/ffi]0;Holmake: ~/regression/cakeml-920/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-920/semantics]0;Holmake: ~/regression/cakeml-920/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
Starting work on cmlPEGTheory
Starting work on fromSexpTheory
Starting work on lexer_implTheory
Starting work on README.md
README.md                                                                                                  OK
fromSexpTheory                                                                                    FAILED! <1>
     case x of NONE => opt = NONE | SOME s => IS_SOME opt  opt = f s
 
 failed.
 Failed to prove theorem sexpopt_SOME.
 
 Exception raised at Tactical.FIRST_ASSUM:
 
 error in quse /home/myreen/regression/cakeml-920/compiler/parsing/fromSexpScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load fromSexpScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
cmlPEGTheory                                                                                         M-KILLED
lexer_implTheory                                                                                     M-KILLED