Job 1712

CakeML:2d10725203d255945a9bed42d277a6bacec99d47
  Encode inc_config rather than config to file [Jan 15 17:40:42]
#857 (eval-bitmaps)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:6b1dbc7559064a70fabbe71836947411103b499e
  Fix INCLUDES for src/coalgebras [Jan 07 05:56:33]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 15 17:50:31 Claimed job
Jan 15 17:50:34 Reusing HOL
Jan 15 17:51:13 Starting developers
Jan 15 17:51:17 Finished developers                                               4s 144MB
Jan 15 17:51:17 Starting developers/bin
Jan 15 17:51:22 Finished developers/bin                                           4s 675MB
Jan 15 17:51:22 Starting semantics/ffi
Jan 15 17:51:32 Finished semantics/ffi                                            9s 212MB
Jan 15 17:51:32 Starting semantics
Jan 15 17:52:54 Finished semantics                                             1m21s 882MB
Jan 15 17:52:54 Starting semantics/proofs
Jan 15 17:56:24 Finished semantics/proofs                                      3m29s   1GB
Jan 15 17:56:24 Starting semantics/alt_semantics
Jan 15 17:56:35 Finished semantics/alt_semantics                                 10s 393MB
Jan 15 17:56:35 Starting semantics/alt_semantics/proofs
Jan 15 17:59:01 Finished semantics/alt_semantics/proofs                        2m26s 899MB
Jan 15 17:59:01 Starting basis/pure
Jan 15 17:59:52 Finished basis/pure                                              50s 880MB
Jan 15 17:59:52 Starting translator
Jan 15 18:02:35 Finished translator                                            2m42s   1GB
Jan 15 18:02:35 Starting compiler/parsing
Jan 15 18:03:47 Finished compiler/parsing                                      1m12s   2GB
Jan 15 18:03:47 Starting characteristic
Jan 15 18:09:30 Finished characteristic                                        5m42s   1GB
Jan 15 18:09:31 Starting translator/monadic
Jan 15 18:11:10 Finished translator/monadic                                    1m38s   1GB
Jan 15 18:11:10 Starting basis
Jan 15 18:21:33 FAILED: basis
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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)/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
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                                                                 (9s)     OK
Starting work on fsFFITheory
clFFITheory                                                                      (10s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                       (0s)     OK
runtimeFFITheory                                                                 (10s)     OK
RuntimeProgTheory                                                                (22s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                      (16s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                 (14s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                               (25s)     OK
fsFFIPropsTheory                                                                 (55s)     OK
ListProgTheory                                                                   (46s)     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                                  (24s)     OK
VectorProgTheory                                                                 (33s)     OK
Starting work on StringProgTheory
StringProgTheory                                                                 (35s)     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                               (33s)     OK
Starting work on IntProgTheory
IntProgTheory                                                                    (33s)     OK
Starting work on RatProgTheory
RatProgTheory                                                                    (41s)     OK
Starting work on CharProgTheory
CharProgTheory                                                                   (27s)     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                                                 (31s)     OK
Starting work on Word8ProgTheory
Word8ProgTheory                                                                  (27s)     OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                                                             (27s)     OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                                                            (35s)     OK
ArrayProgTheory                                                                  (77s)     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                                                    (53s)     OK
Starting work on HashtableProgTheory
ArrayProofTheory                                                                 (61s)     OK
HashtableProgTheory                                                              (57s)     OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
HashtableProofTheory                                                             (34s)FAIL<1>
 
 a b hf hfv cmp cmpv size sizev ar.
   NUM size sizev  (a --> NUM) hf hfv 
   (a --> a --> ORDERING_TYPE) cmp cmpv  TotOrd cmp 
   app p Hashtable_empty_v [sizev; hfv; cmpv] emp
     (POSTv htv. HASHTABLE a b hf cmp FEMPTY htv)
 
 failed.
 Failed to prove theorem hashtable_empty_spec.
 Uncaught exception: HOL_ERR {message = "goal not an exists (THEN1 on line 519) (THEN1 on line 520) (THEN1 on line 521) (THEN1 on line 522) (THEN1 on line 498) (THEN1 on line 527) (THEN1 on line 530) (THEN1 on line 534) (THEN1 on line 547) (THEN1 on line 551) (THEN1 on line 552) (THEN1 on line 553) (THEN1 on line 554) (THEN1 on line 557)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
CommandLineProgTheory                                                            (34s)MKILLED