Job 1951

CakeML:42712c3f0757b8330cf98aaa30c0f4ed2800a50c
  Make bootstrap test ./cake --types output of basis [Jul 04 20:44:29]
#895 (issue894)
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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jul 04 21:10:51 Claimed job
Jul 04 21:12:13 Building HOL
Jul 04 21:24:36 Starting developers
Jul 04 21:24:41 Finished developers                                               5s 101MB
Jul 04 21:24:42 Starting developers/bin
Jul 04 21:26:26 Finished developers/bin                                        1m43s   1GB
Jul 04 21:26:26 Starting semantics/ffi
Jul 04 21:26:37 Finished semantics/ffi                                           11s 191MB
Jul 04 21:26:37 Starting semantics
Jul 04 21:29:29 Finished semantics                                             2m51s   1GB
Jul 04 21:29:30 Starting semantics/proofs
Jul 04 21:37:22 Finished semantics/proofs                                      7m51s   1GB
Jul 04 21:37:22 Starting semantics/alt_semantics
Jul 04 21:37:52 Finished semantics/alt_semantics                                 29s 545MB
Jul 04 21:37:52 Starting semantics/alt_semantics/proofs
Jul 04 21:50:39 Finished semantics/alt_semantics/proofs                       12m46s   1GB
Jul 04 21:50:39 Starting basis/pure
Jul 04 21:54:31 Finished basis/pure                                            3m52s 995MB
Jul 04 21:54:32 Starting translator
Jul 04 21:58:29 Finished translator                                            3m57s   1GB
Jul 04 21:58:30 Starting compiler/parsing
Jul 04 21:58:53 FAILED: compiler/parsing
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
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.855s) 
Starting work on fromSexpTheory
fromSexpTheory                                    compiler/parsing (13s)FAIL<1>
 no solution found
 error in quse /home/cake/oven/regression/cakeml-1951/compiler/parsing/fromSexpScript.sml : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /home/cake/oven/regression/cakeml-1951/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 (20s)MKILLED
lexer_implTheory                                  compiler/parsing (20s)MKILLED