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:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 76MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 9s 306MB
Starting semantics
Finished semantics 1m27s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m31s 1GB
Starting basis/pure
Finished basis/pure 53s 1GB
Starting translator
Finished translator 3m17s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m11s 3GB
Starting characteristic
Finished characteristic 5m39s 3GB
Starting translator/monadic
Finished translator/monadic 1m45s 2GB
Starting basis
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)/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 real: 0s user: 0s OK
Starting work on runtimeFFITheory
MarshallingTheory real: 11s user: 11s OK
Starting work on fsFFITheory
runtimeFFITheory real: 12s user: 11s OK
Starting work on basis_ffi.o
basis_ffi.o real: 0s user: 0s OK
clFFITheory real: 13s user: 12s OK
RuntimeProgTheory real: 27s user: 26s OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory real: 17s user: 16s OK
Starting work on fsFFIPropsTheory
OptionProgTheory real: 18s user: 17s OK
Starting work on ListProgTheory
RuntimeProofTheory real: 30s user: 29s OK
fsFFIPropsTheory real: 59s user: 58s OK
ListProgTheory real: 49s user: 47s OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory real: 30s user: 29s OK
VectorProgTheory real: 34s user: 33s OK
Starting work on StringProgTheory
StringProgTheory real: 36s user: 35s OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory real: 35s user: 34s OK
Starting work on IntProgTheory
IntProgTheory real: 37s user: 35s OK
Starting work on RatProgTheory
RatProgTheory real: 44s user: 42s OK
Starting work on CharProgTheory
CharProgTheory real: 32s user: 31s OK
Starting work on Word64ProgTheory
Word64ProgTheory real: 33s user: 31s OK
Starting work on Word8ProgTheory
Word8ProgTheory real: 32s user: 30s OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory real: 31s user: 29s OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory real: 40s user: 39s OK
ArrayProgTheory real: 75s user: 73s OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory real: 57s user: 56s OK
Starting work on HashtableProgTheory
ArrayProofTheory real: 65s user: 64s OK
HashtableProgTheory real: 55s user: 54s OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
HashtableProofTheory real: 40s user: 38sFAIL<1>
(POSTv htv. HASHTABLE a b hf cmp FEMPTY htv)
failed.
Failed to prove theorem hashtable_empty_spec.
Exception raised at Q.EXISTS_TAC:
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)
error in quse /home/myreen/regression/cakeml-1441/basis/HashtableProofScript.sml : 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"}
error in load /home/myreen/regression/cakeml-1441/basis/HashtableProofScript : 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"}
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