Job 1105

CakeML:16b2b4eeedb24ac9ffb91eac4b030d724864b29e
  Fix a proof and adjust some indenting [Nov 28 02:29:02]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 28 02:36:36 Claimed job
Nov 28 02:36:38 Reusing HOL
Nov 28 02:37:30 Starting developers
Nov 28 02:37:34 Finished developers                                               3s 101MB
Nov 28 02:37:35 Starting developers/bin
Nov 28 02:37:42 Finished developers/bin                                           6s 960MB
Nov 28 02:37:42 Starting semantics/ffi
Nov 28 02:37:51 Finished semantics/ffi                                            9s 219MB
Nov 28 02:37:52 Starting semantics
Nov 28 02:39:09 Finished semantics                                             1m17s   1GB
Nov 28 02:39:09 Starting semantics/proofs
Nov 28 02:42:09 Finished semantics/proofs                                      2m59s 954MB
Nov 28 02:42:09 Starting semantics/alt_semantics
Nov 28 02:42:16 Finished semantics/alt_semantics                                  7s 288MB
Nov 28 02:42:16 Starting semantics/alt_semantics/proofs
Nov 28 02:44:04 Finished semantics/alt_semantics/proofs                        1m47s 700MB
Nov 28 02:44:04 Starting basis/pure
Nov 28 02:44:51 Finished basis/pure                                              46s 852MB
Nov 28 02:44:51 Starting translator
Nov 28 02:46:39 Finished translator                                            1m48s   1GB
Nov 28 02:46:40 Starting compiler/parsing
Nov 28 02:47:45 Finished compiler/parsing                                      1m04s   2GB
Nov 28 02:47:45 Starting characteristic
Nov 28 02:52:57 Finished characteristic                                        5m12s   2GB
Nov 28 02:52:57 Starting translator/monadic
Nov 28 02:54:27 Finished translator/monadic                                    1m29s   1GB
Nov 28 02:54:28 Starting basis
Nov 28 03:03:42 FAILED: basis
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
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:   10s  user:    9s     OK
Starting work on fsFFITheory
clFFITheory                                     real:   11s  user:   10s     OK
Starting work on basis_ffi.o
basis_ffi.o                                     real:    0s  user:    0s     OK
runtimeFFITheory                                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:   14s  user:   13s     OK
Starting work on ListProgTheory
RuntimeProofTheory                              real:   24s  user:   23s     OK
fsFFIPropsTheory                                real:   51s  user:   50s     OK
ListProgTheory                                  real:   42s  user:   41s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                 real:   24s  user:   23s     OK
VectorProgTheory                                real:   29s  user:   28s     OK
Starting work on StringProgTheory
StringProgTheory                                real:   31s  user:   29s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                              real:   30s  user:   29s     OK
Starting work on IntProgTheory
IntProgTheory                                   real:   30s  user:   28s     OK
Starting work on RatProgTheory
RatProgTheory                                   real:   37s  user:   36s     OK
Starting work on CharProgTheory
CharProgTheory                                  real:   23s  user:   22s     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                real:   26s  user:   25s     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:   36s  user:   35s     OK
ArrayProgTheory                                 real:   67s  user:   66s     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                   real:   49s  user:   48s     OK
Starting work on HashtableProgTheory
ArrayProofTheory                                real:   69s  user:   68s     OK
HashtableProgTheory                             real:   59s  user:   57s     OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
HashtableProofTheory                            real:   35s  user:   33sFAIL<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