CakeML:4cd953474ce72ae40ffdbb303741a04124d4fb2a
prove word_to_word_compile_semantics
#909 (word_to_word_Pancake)
Merging into:8f9eeb4f6d657077aca5ed92c7f20bd8c35befef
Remove failing diminish_srw_ss
HOL:893dead4b6f59a9be7fc251533d0a5ee77e12e56
Add some simple test for bitArithLib and document in next-release.md
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 3s 112MB
Starting developers/bin
Finished developers/bin 7s 1GB
Starting semantics/ffi
Finished semantics/ffi 12s 262MB
Starting semantics
Finished semantics 3m30s 2GB
Starting semantics/proofs
Finished semantics/proofs 9m15s 2GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 36s 520MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 12m19s 2GB
Starting basis/pure
Finished basis/pure 1m12s 1GB
Starting translator
Finished translator 4m01s 3GB
Starting compiler/parsing
Finished compiler/parsing 1m40s 5GB
Starting characteristic
Finished characteristic 6m56s 4GB
Starting translator/monadic
Finished translator/monadic 2m03s 2GB
Starting basis
FAILED: basis
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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
Scanned 28 directories
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md (0s) OK
Starting work on runtimeFFITheory
MarshallingTheory (13s) OK
Starting work on fsFFITheory
runtimeFFITheory (15s) OK
Starting work on basis_ffi.o
basis_ffi.o (0s) OK
clFFITheory (17s) OK
RuntimeProgTheory (30s) OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory (24s) OK
Starting work on fsFFIPropsTheory
OptionProgTheory (18s) OK
Starting work on ListProgTheory
RuntimeProofTheory (32s) OK
fsFFIPropsTheory (58s) OK
ListProgTheory (55s) OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory (28s) OK
VectorProgTheory (35s) OK
Starting work on StringProgTheory
StringProgTheory (39s) OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory (39s) OK
Starting work on IntProgTheory
IntProgTheory (39s) OK
Starting work on PrettyPrinterProgTheory
PrettyPrinterProgTheory (27s) OK
Starting work on RatProgTheory
RatProgTheory (46s) OK
Starting work on CharProgTheory
CharProgTheory (33s) OK
Starting work on Word64ProgTheory
Word64ProgTheory (35s) OK
Starting work on Word8ProgTheory
Word8ProgTheory (34s) OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory (32s) OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory (43s) OK
ArrayProgTheory (82s) OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory (69s) OK
Starting work on HashtableProgTheory
ArrayProofTheory (78s) OK
HashtableProgTheory (61s) OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
CommandLineProgTheory (45s) OK
Starting work on CommandLineProofTheory
Starting work on DoubleProgTheory
DoubleProgTheory (67s) OK
Starting work on DoubleFFITheory
Starting work on MarshallingProgTheory
DoubleFFITheory (24s) OK
Starting work on DoubleProofTheory
CommandLineProofTheory (105s) OK
MarshallingProgTheory (69s) OK
Starting work on TextIOProgTheory
HashtableProofTheory (197s) OK
DoubleProofTheory (198s) OK
TextIOProgTheory (189s) OK
Starting work on TextIOProofTheory
TextIOProofTheory (32m) OK
Starting work on basisProgTheory
Starting work on basis_ffiTheory
basisProgTheory (51s) OK
Starting work on UnsafeProgTheory
basis_ffiTheory (69s) OK
UnsafeProgTheory (36s) OK
Starting work on UnsafeProofTheory
UnsafeProofTheory (11s)FAIL<1>
Run out of store - interrupting threads
error in quse /home/myreen/regression/cakeml-1990/basis/TextIOProofTheory.sml : Interrupt
error in load $(CAKEMLDIR)/basis/TextIOProofTheory : Interrupt
error in load $(CAKEMLDIR)/basis/basisProgTheory : Interrupt
error in load $(CAKEMLDIR)/basis/UnsafeProgTheory : Interrupt
error in load /home/myreen/regression/cakeml-1990/basis/UnsafeProofScript : Interrupt
Uncaught exception: Interrupt