Job 1798

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:42596dd3aaa8b5ce1a7b27086d9b979fe5f7838a
  Fixes following changes to Define in HOL [Feb 24 20:23:43]
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
  Refine definition of what it is to be a vacuous pattern [Feb 25 06:46:55]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 25 10:28:04 Claimed job
Feb 25 10:28:06 Reusing HOL
Feb 25 10:28:20 Starting developers
Feb 25 10:28:24 Finished developers                                               4s 121MB
Feb 25 10:28:24 Starting developers/bin
Feb 25 10:28:28 Finished developers/bin                                           4s 674MB
Feb 25 10:28:29 Starting semantics/ffi
Feb 25 10:28:39 Finished semantics/ffi                                           10s 243MB
Feb 25 10:28:39 Starting semantics
Feb 25 10:30:41 Finished semantics                                             2m01s   1GB
Feb 25 10:30:42 Starting semantics/proofs
Feb 25 10:34:18 Finished semantics/proofs                                      3m36s   1GB
Feb 25 10:34:19 Starting semantics/alt_semantics
Feb 25 10:34:35 Finished semantics/alt_semantics                                 16s 492MB
Feb 25 10:34:35 Starting semantics/alt_semantics/proofs
Feb 25 10:37:03 Finished semantics/alt_semantics/proofs                        2m27s 910MB
Feb 25 10:37:03 Starting basis/pure
Feb 25 10:38:06 Finished basis/pure                                            1m03s 882MB
Feb 25 10:38:06 Starting translator
Feb 25 10:41:09 Finished translator                                            3m02s   1GB
Feb 25 10:41:09 Starting compiler/parsing
Feb 25 10:42:23 Finished compiler/parsing                                      1m13s   2GB
Feb 25 10:42:23 Starting characteristic
Feb 25 10:48:47 Finished characteristic                                        6m24s   2GB
Feb 25 10:48:47 Starting translator/monadic
Feb 25 10:50:40 Finished translator/monadic                                    1m52s   1GB
Feb 25 10:50:40 Starting basis
Feb 25 11:52:59 FAILED: basis
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/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanned 28 directories
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md                                                           (0s)     OK
Starting work on runtimeFFITheory
MarshallingTheory                                                  (11s)     OK
Starting work on fsFFITheory
runtimeFFITheory                                                   (12s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                         (0s)     OK
clFFITheory                                                        (14s)     OK
RuntimeProgTheory                                                  (27s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                        (22s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                   (17s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                 (28s)     OK
fsFFIPropsTheory                                                   (54s)     OK
ListProgTheory                                                     (60m)FAIL<Signal 9>
 Saved theorem _______ "nsLookup_ListProg_env_37_pfun_eqs"
 Adding nsLookup representation thms for [ListProg_env_37]
 Saved theorem _______ "collate_v_thm"
 Saved theorem _______ "ZIP_ind"
 Translating zip
 Saved theorem _______ "zip_side_rules"
 Saved theorem _______ "zip_side_ind"
 Saved theorem _______ "zip_side_strongind"
 Saved theorem _______ "zip_side_cases"
 Saved theorem _______ "zip_side_def"