Job 921

CakeML: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:33:31 Claimed job
Jun 28 19:33:33 Reusing HOL
Jun 28 19:33:38 Starting developers
Jun 28 19:33:38 Finished developers                                               0s  21MB
Jun 28 19:33:39 Starting developers/bin
Jun 28 19:33:42 Finished developers/bin                                           3s 144MB
Jun 28 19:33:42 Starting semantics/ffi
Jun 28 19:33:50 Finished semantics/ffi                                            7s 220MB
Jun 28 19:33:50 Starting semantics
Jun 28 19:35:07 Finished semantics                                             1m16s   1GB
Jun 28 19:35:08 Starting semantics/proofs
Jun 28 19:38:07 Finished semantics/proofs                                      2m59s   1GB
Jun 28 19:38:07 Starting semantics/alt_semantics
Jun 28 19:38:14 Finished semantics/alt_semantics                                  5s 302MB
Jun 28 19:38:14 Starting semantics/alt_semantics/proofs
Jun 28 19:40:00 Finished semantics/alt_semantics/proofs                        1m45s 715MB
Jun 28 19:40:00 Starting basis/pure
Jun 28 19:40:44 Finished basis/pure                                              43s 686MB
Jun 28 19:40:44 Starting translator
Jun 28 19:42:22 Finished translator                                            1m37s   1GB
Jun 28 19:42:23 Starting compiler/parsing
Jun 28 19:43:02 FAILED: compiler/parsing
]0;Holmake: .]0;Holmake: ~/regression/cakeml-921/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-921/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-921/misc]0;Holmake: ~/regression/cakeml-921/developers]0;Holmake: ~/regression/cakeml-921/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-921/misc]0;Holmake: ~/regression/cakeml-921/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-921/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-921/misc]0;Holmake: ~/regression/cakeml-921/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-921/semantics]0;Holmake: ~/regression/cakeml-921/semantics/ffi]0;Holmake: ~/regression/cakeml-921/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-921/semantics]0;Holmake: ~/regression/cakeml-921/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-921/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