Job 1949

CakeML:187e6991cdce21d86f639d8a88b3aa9020117c95
  Merge pull request #892 from CakeML/double-type-new [Jul 01 10:20:40]
HOL:36b541e828806d911b2fee3e1cb1e3298068dfd9
  Tidy up some simpleSexp proofs [Jul 01 07:00:10]
Machine:oven3

Jul 04 17:00:48 Claimed job
Jul 04 17:01:02 Building HOL
Jul 04 17:24:46 Starting developers
Jul 04 17:24:56 Finished developers                                               9s 132MB
Jul 04 17:24:56 Starting developers/bin
Jul 04 17:25:09 Finished developers/bin                                          12s   1GB
Jul 04 17:25:09 Starting semantics/ffi
Jul 04 17:25:35 Finished semantics/ffi                                           25s 264MB
Jul 04 17:25:35 Starting semantics
Jul 04 17:30:55 Finished semantics                                             5m19s   1GB
Jul 04 17:30:55 Starting semantics/proofs
Jul 04 17:47:24 Finished semantics/proofs                                     16m28s   1GB
Jul 04 17:47:24 Starting semantics/alt_semantics
Jul 04 17:48:24 Finished semantics/alt_semantics                               1m00s 561MB
Jul 04 17:48:25 Starting semantics/alt_semantics/proofs
Jul 04 18:14:28 Finished semantics/alt_semantics/proofs                       26m03s   1GB
Jul 04 18:14:29 Starting basis/pure
Jul 04 18:22:14 Finished basis/pure                                            7m44s 884MB
Jul 04 18:22:14 Starting translator
Jul 04 18:30:12 Finished translator                                            7m58s   1GB
Jul 04 18:30:13 Starting compiler/parsing
Jul 04 18:30:54 FAILED: compiler/parsing
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 19 directories
Starting work on simpleSexpTheory
Starting work on README.md
Starting work on cmlPEGTheory
Starting work on lexer_implTheory
README.md                                                                                                                                                                           compiler/parsing  (0s)     OK
simpleSexpTheory                                                                                                                                              examples/formal-languages/context-free (11s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1]                                                                                                                                (11.791s) 
Starting work on fromSexpTheory
fromSexpTheory                                                                                                                                                                      compiler/parsing (24s)FAIL<1>
 no solution found
 error in quse /root/regression/cakeml-1949/compiler/parsing/fromSexpScript.sml : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /root/regression/cakeml-1949/compiler/parsing/fromSexpScript : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Proof of 
 
 s. strip_sxcons s = NONE  sexplist p s = NONE
 
 failed.
 Failed to prove theorem strip_sxcons_FAIL_sexplist_FAIL.
 Uncaught exception: HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
cmlPEGTheory                                                                                                                                                                        compiler/parsing (37s)MKILLED
lexer_implTheory                                                                                                                                                                    compiler/parsing (37s)MKILLED