CakeML:82a6a52180a50be3f374f0be862f54087aefae18
Move alt_semantics down the build-seq temporarily
#811 (eval)
Merging into:3c6495906dc020e093e2f5cf101cea1cba2fc468
Fix breakage caused by change to sorted_map in HOL
HOL:07dca05c1eb441bb9b18556ae55f275d2518bade
Fix bugs in Makefiles/lib files preventing Lassie from compiling
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Building HOL
Starting developers
Finished developers 4s 108MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 238MB
Starting semantics
Finished semantics 1m41s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m58s 1GB
Starting basis/pure
Finished basis/pure 3m08s 926MB
Starting translator
Finished translator 3m53s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m33s 1GB
Starting characteristic
Finished characteristic 6m20s 2GB
Starting translator/monadic
Finished translator/monadic 1m47s 1GB
Starting basis
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)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
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: 12s user: 11s OK
Starting work on fsFFITheory
runtimeFFITheory real: 13s user: 12s OK
Starting work on basis_ffi.o
basis_ffi.o real: 0s user: 0s OK
clFFITheory real: 15s user: 14s OK
fsFFITheory real: 17s user: 16s OK
Starting work on fsFFIPropsTheory
RuntimeProgTheory real: 30s user: 28s OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
OptionProgTheory real: 18s user: 17s OK
Starting work on ListProgTheory
RuntimeProofTheory real: 29s user: 28s OK
fsFFIPropsTheory real: 66s user: 64s OK
ListProgTheory real: 55s user: 54s OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory real: 28s user: 27s OK
VectorProgTheory real: 36s user: 34s OK
Starting work on StringProgTheory
StringProgTheory real: 37s user: 35s OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory real: 41s user: 40s OK
Starting work on IntProgTheory
IntProgTheory real: 39s user: 38s OK
Starting work on RatProgTheory
RatProgTheory real: 46s user: 45s OK
Starting work on CharProgTheory
CharProgTheory real: 33s user: 31s OK
Starting work on Word64ProgTheory
Word64ProgTheory real: 33s user: 32s OK
Starting work on Word8ProgTheory
Word8ProgTheory real: 31s user: 30s OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory real: 32s user: 30s OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory real: 41s user: 39s OK
ArrayProgTheory real: 80s user: 78s OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory real: 62s user: 60s OK
Starting work on HashtableProgTheory
ArrayProofTheory real: 77s user: 75s OK
HashtableProgTheory real: 60s user: 58s OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
HashtableProofTheory real: 40s user: 38sFAIL<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 M-KILLED