Job 1950

CakeML:4cba31259526004a87507ef2f43cc46a0ef0272d
  Merge remote-tracking branch 'origin/master' into gh859 [Jul 04 21:00:13]
#862 (gh859)
Merging into: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:stove 4.15.0-143-generic x86_64 GNU/Linux

Jul 04 21:01:35 Claimed job
Jul 04 21:01:41 Building HOL
Jul 04 21:12:55 Starting developers
Jul 04 21:13:00 Finished developers                                               4s  95MB
Jul 04 21:13:00 Starting developers/bin
Jul 04 21:13:06 Finished developers/bin                                           6s   1GB
Jul 04 21:13:06 Starting semantics/ffi
Jul 04 21:13:16 Finished semantics/ffi                                            9s 220MB
Jul 04 21:13:16 Starting semantics
Jul 04 21:15:56 Finished semantics                                             2m39s   1GB
Jul 04 21:15:56 Starting semantics/proofs
Jul 04 21:23:04 Finished semantics/proofs                                      7m07s   1GB
Jul 04 21:23:04 Starting semantics/alt_semantics
Jul 04 21:23:32 Finished semantics/alt_semantics                                 28s 552MB
Jul 04 21:23:33 Starting semantics/alt_semantics/proofs
Jul 04 21:35:15 Finished semantics/alt_semantics/proofs                       11m42s   1GB
Jul 04 21:35:15 Starting basis/pure
Jul 04 21:38:48 Finished basis/pure                                            3m32s 913MB
Jul 04 21:38:48 Starting translator
Jul 04 21:42:32 Finished translator                                            3m43s   1GB
Jul 04 21:42:32 Starting compiler/parsing
Jul 04 21:42:53 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  (5s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1]                                       (5.390s) 
Starting work on fromSexpTheory
fromSexpTheory                                                                            compiler/parsing (13s)FAIL<1>
 s. strip_sxcons s = NONE  sexplist p s = NONE
 
 failed.
 Failed to prove theorem strip_sxcons_FAIL_sexplist_FAIL.
 
 Exception raised at folTools.FOL_FIND:
 no solution found
 error in quse /home/cug/hk324/cml-regression/cakeml-1950/compiler/parsing/fromSexpScript.sml : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /home/cug/hk324/cml-regression/cakeml-1950/compiler/parsing/fromSexpScript : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Uncaught exception: HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
cmlPEGTheory                                                                              compiler/parsing (20s)MKILLED
lexer_implTheory                                                                          compiler/parsing (19s)MKILLED