Job 1106

CakeML:f18a8b01f422c0b17f5a557281b2ea59c8b5fa7d
  Fix a broken proof [Nov 28 02:44:34]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 28 03:01:36 Claimed job
Nov 28 03:01:38 Reusing HOL
Nov 28 03:02:28 Starting developers
Nov 28 03:02:32 Finished developers                                               3s 124MB
Nov 28 03:02:32 Starting developers/bin
Nov 28 03:02:38 Finished developers/bin                                           5s 964MB
Nov 28 03:02:38 Starting semantics/ffi
Nov 28 03:02:47 Finished semantics/ffi                                            9s 232MB
Nov 28 03:02:47 Starting semantics
Nov 28 03:04:00 Finished semantics                                             1m12s   1GB
Nov 28 03:04:00 Starting semantics/proofs
Nov 28 03:06:48 Finished semantics/proofs                                      2m47s   1GB
Nov 28 03:06:48 Starting semantics/alt_semantics
Nov 28 03:06:55 Finished semantics/alt_semantics                                  7s 294MB
Nov 28 03:06:55 Starting semantics/alt_semantics/proofs
Nov 28 03:08:39 Finished semantics/alt_semantics/proofs                        1m43s 902MB
Nov 28 03:08:39 Starting basis/pure
Nov 28 03:09:23 Finished basis/pure                                              43s 759MB
Nov 28 03:09:23 Starting translator
Nov 28 03:11:04 Finished translator                                            1m41s   1GB
Nov 28 03:11:05 Starting compiler/parsing
Nov 28 03:12:06 Finished compiler/parsing                                      1m01s   1GB
Nov 28 03:12:06 Starting characteristic
Nov 28 03:17:08 Finished characteristic                                        5m01s   1GB
Nov 28 03:17:08 Starting translator/monadic
Nov 28 03:18:35 Finished translator/monadic                                    1m27s   1GB
Nov 28 03:18:35 Starting basis
Nov 28 03:27:56 FAILED: basis
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)/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/lem_lib_stub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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                                       real:    0s  user:    0s     OK
Starting work on runtimeFFITheory
MarshallingTheory                               real:    9s  user:    8s     OK
Starting work on fsFFITheory
clFFITheory                                     real:   10s  user:    9s     OK
Starting work on basis_ffi.o
basis_ffi.o                                     real:    0s  user:    0s     OK
runtimeFFITheory                                real:   10s  user:    9s     OK
RuntimeProgTheory                               real:   23s  user:   22s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                     real:   14s  user:   13s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                real:   13s  user:   12s     OK
Starting work on ListProgTheory
RuntimeProofTheory                              real:   23s  user:   22s     OK
fsFFIPropsTheory                                real:   48s  user:   46s     OK
ListProgTheory                                  real:   42s  user:   41s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                 real:   21s  user:   20s     OK
VectorProgTheory                                real:   29s  user:   28s     OK
Starting work on StringProgTheory
StringProgTheory                                real:   31s  user:   30s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                              real:   35s  user:   33s     OK
Starting work on IntProgTheory
IntProgTheory                                   real:   29s  user:   28s     OK
Starting work on RatProgTheory
RatProgTheory                                   real:   39s  user:   37s     OK
Starting work on CharProgTheory
CharProgTheory                                  real:   22s  user:   21s     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                real:   27s  user:   26s     OK
Starting work on Word8ProgTheory
Word8ProgTheory                                 real:   25s  user:   24s     OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                            real:   25s  user:   24s     OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                           real:   37s  user:   36s     OK
ArrayProgTheory                                 real:   72s  user:   70s     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                   real:   48s  user:   46s     OK
Starting work on HashtableProgTheory
ArrayProofTheory                                real:   66s  user:   64s     OK
HashtableProgTheory                             real:   56s  user:   54s     OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
CommandLineProgTheory                           real:   35s  user:   33s     OK
Starting work on CommandLineProofTheory
Starting work on DoubleProgTheory
HashtableProofTheory                            real:   35s  user:   34sFAIL<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 = "first subgoal not solved by second tactic (THEN1 on line 521) (THEN1 on line 522) (THEN1 on line 523) (THEN1 on line 505) (THEN1 on line 501) (THEN1 on line 498) (THEN1 on line 526) (THEN1 on line 492)", origin_function = "THEN1", origin_structure = "Tactical"}
CommandLineProofTheory                                                  M-KILLED
DoubleProgTheory                                                        M-KILLED