Job 1697

CakeML:761b33d5c59b62a50a3543bc67362744ff2f598a
  Move a forgotten Lem file and update README.md files [Dec 18 17:13:53]
HOL:4701a25198bb2dd55129bbf8269c0660080ce56c
  Tweak INDUCT_THEN to allow induction thms with hypotheses [Dec 17 06:14:51]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 21 05:15:01 Claimed job
Dec 21 05:15:10 Reusing HOL
Dec 21 05:15:49 Starting developers
Dec 21 05:15:54 Finished developers                                               4s 101MB
Dec 21 05:15:54 Starting developers/bin
Dec 21 05:16:00 Finished developers/bin                                           5s 670MB
Dec 21 05:16:00 Starting semantics/ffi
Dec 21 05:16:09 Finished semantics/ffi                                            8s 192MB
Dec 21 05:16:09 Starting semantics
Dec 21 05:17:35 Finished semantics                                             1m25s   1GB
Dec 21 05:17:35 Starting semantics/proofs
Dec 21 05:21:24 Finished semantics/proofs                                      3m48s   1GB
Dec 21 05:21:24 Starting semantics/alt_semantics
Dec 21 05:21:36 Finished semantics/alt_semantics                                 11s 336MB
Dec 21 05:21:36 Starting semantics/alt_semantics/proofs
Dec 21 05:24:13 Finished semantics/alt_semantics/proofs                        2m36s 936MB
Dec 21 05:24:13 Starting basis/pure
Dec 21 05:25:04 Finished basis/pure                                              50s 653MB
Dec 21 05:25:04 Starting translator
Dec 21 05:28:02 Finished translator                                            2m57s   1GB
Dec 21 05:28:02 Starting compiler/parsing
Dec 21 05:28:13 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
Starting work on README.md
Starting work on cmlPEGTheory
Starting work on fromSexpTheory
Starting work on lexer_implTheory
README.md                                                           (0s)     OK
fromSexpTheory                                                      (8s)FAIL<1>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 Saved definition ____ "decode_control_def"
 Saved induction _____ "decode_control_ind"
 error in quse /home/cake/oven/regression/cakeml-1697/compiler/parsing/fromSexpScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1697/compiler/parsing/fromSexpScript : Fail "Static Errors"
 Saved theorem _______ "EVERY_isPrint_encode_control"
 /home/cake/oven/regression/cakeml-1697/compiler/parsing/fromSexpScript.sml:175: error: Value or constructor (LIST_LENGTH_2) has not been declared in structure quantHeuristicsTheory
 Found near [quantHeuristicsTheory.LIST_LENGTH_2]
 Uncaught exception: Fail "Static Errors"
cmlPEGTheory                                                        (9s)MKILLED
lexer_implTheory                                                    (9s)MKILLED