Job 1107

CakeML:dc281bfd93e26d5307a5c595782b7a54d50d8aca
  Fix silly proof failure due to REPLICATE [Nov 28 06:05:02]
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 06:07:58 Claimed job
Nov 28 06:08:00 Reusing HOL
Nov 28 06:08:45 Starting developers
Nov 28 06:08:49 Finished developers                                               3s  84MB
Nov 28 06:08:49 Starting developers/bin
Nov 28 06:08:55 Finished developers/bin                                           5s 964MB
Nov 28 06:08:55 Starting semantics/ffi
Nov 28 06:09:04 Finished semantics/ffi                                            9s 244MB
Nov 28 06:09:04 Starting semantics
Nov 28 06:10:17 Finished semantics                                             1m12s   1GB
Nov 28 06:10:17 Starting semantics/proofs
Nov 28 06:13:07 Finished semantics/proofs                                      2m49s 906MB
Nov 28 06:13:07 Starting semantics/alt_semantics
Nov 28 06:13:14 Finished semantics/alt_semantics                                  7s 296MB
Nov 28 06:13:14 Starting semantics/alt_semantics/proofs
Nov 28 06:14:57 Finished semantics/alt_semantics/proofs                        1m43s 813MB
Nov 28 06:14:57 Starting basis/pure
Nov 28 06:15:42 Finished basis/pure                                              45s 627MB
Nov 28 06:15:42 Starting translator
Nov 28 06:17:23 Finished translator                                            1m40s   1GB
Nov 28 06:17:23 Starting compiler/parsing
Nov 28 06:18:25 Finished compiler/parsing                                      1m01s   2GB
Nov 28 06:18:25 Starting characteristic
Nov 28 06:23:32 Finished characteristic                                        5m06s   1GB
Nov 28 06:23:32 Starting translator/monadic
Nov 28 06:24:59 Finished translator/monadic                                    1m26s   1GB
Nov 28 06:24:59 Starting basis
Nov 28 06:34:13 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
runtimeFFITheory                                real:    9s  user:    8s     OK
Starting work on basis_ffi.o
basis_ffi.o                                     real:    0s  user:    0s     OK
clFFITheory                                     real:   10s  user:    9s     OK
RuntimeProgTheory                               real:   22s  user:   21s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                     real:   14s  user:   13s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                real:   12s  user:   11s     OK
Starting work on ListProgTheory
RuntimeProofTheory                              real:   23s  user:   22s     OK
fsFFIPropsTheory                                real:   49s  user:   47s     OK
ListProgTheory                                  real:   40s  user:   39s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                 real:   22s  user:   21s     OK
VectorProgTheory                                real:   29s  user:   28s     OK
Starting work on StringProgTheory
StringProgTheory                                real:   31s  user:   30s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                              real:   33s  user:   32s     OK
Starting work on IntProgTheory
IntProgTheory                                   real:   27s  user:   26s     OK
Starting work on RatProgTheory
RatProgTheory                                   real:   39s  user:   38s     OK
Starting work on CharProgTheory
CharProgTheory                                  real:   21s  user:   20s     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                real:   27s  user:   26s     OK
Starting work on Word8ProgTheory
Word8ProgTheory                                 real:   26s  user:   25s     OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                            real:   26s  user:   25s     OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                           real:   35s  user:   34s     OK
ArrayProgTheory                                 real:   76s  user:   75s     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                   real:   49s  user:   47s     OK
Starting work on HashtableProgTheory
ArrayProofTheory                                real:   65s  user:   64s     OK
HashtableProgTheory                             real:   51s  user:   50s     OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
HashtableProofTheory                            real:   33s  user:   32sFAIL<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"}
CommandLineProgTheory                                                   M-KILLED