CakeML:cd2447c3d3fa7f4bc813a2c46a08c3b5403c31fc
Update lem files and regenerate lem output
#692 (match-refactor-2)
Merging into:5752e21fdd0a5da28d3bec757206728debc27640
Merge pull request #702 from CakeML/bufferedio
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
adding back combinTheory dependency to hhExportLib
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 77MB
Starting developers/bin
Finished developers/bin 6s 960MB
Starting semantics/ffi
Finished semantics/ffi 10s 202MB
Starting semantics
Finished semantics 1m20s 1GB
Starting semantics/proofs
Resuming semantics/proofs
Finished semantics/proofs 2m04s 833MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 7s 325MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m05s 887MB
Starting basis/pure
Finished basis/pure 49s 644MB
Starting translator
Finished translator 2m32s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m09s 1GB
Starting characteristic
Finished characteristic 5m43s 1GB
Starting translator/monadic
Finished translator/monadic 1m33s 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)/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: 10s OK
Starting work on fsFFITheory
clFFITheory real: 11s user: 11s OK
Starting work on basis_ffi.o
basis_ffi.o real: 0s user: 0s OK
runtimeFFITheory real: 11s user: 10s OK
RuntimeProgTheory real: 23s user: 22s OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory real: 15s user: 14s OK
Starting work on fsFFIPropsTheory
OptionProgTheory real: 14s user: 13s OK
Starting work on ListProgTheory
RuntimeProofTheory real: 25s user: 24s OK
fsFFIPropsTheory real: 54s user: 53s OK
ListProgTheory real: 45s user: 43s 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: 32s user: 31s OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory real: 36s user: 34s OK
Starting work on IntProgTheory
IntProgTheory real: 33s user: 32s OK
Starting work on RatProgTheory
RatProgTheory real: 40s user: 39s OK
Starting work on CharProgTheory
CharProgTheory real: 25s user: 24s OK
Starting work on Word64ProgTheory
Word64ProgTheory real: 29s user: 28s 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: 36s user: 34s OK
ArrayProgTheory real: 82s user: 79s OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory real: 54s user: 52s OK
Starting work on HashtableProgTheory
ArrayProofTheory real: 71s user: 70s OK
HashtableProgTheory real: 52s user: 51s OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
CommandLineProgTheory real: 38s user: 37s OK
Starting work on CommandLineProofTheory
Starting work on DoubleProgTheory
DoubleProgTheory real: 46s user: 44s OK
Starting work on DoubleFFITheory
Starting work on MarshallingProgTheory
DoubleFFITheory real: 16s user: 15s OK
Starting work on DoubleProofTheory
CommandLineProofTheory real: 98s user: 96s OK
MarshallingProgTheory real: 59s user: 57s OK
Starting work on TextIOProgTheory
HashtableProofTheory real: 183s user: 180s OK
TextIOProgTheory real: 117s user: 115s OK
Starting work on PrettyPrinterProgTheory
Starting work on TextIOProofTheory
DoubleProofTheory real: 172s user: 170s OK
PrettyPrinterProgTheory real: 28s user: 26s OK
TextIOProofTheory real: 461s user: 454sFAIL<1>
INSTREAM_BUFFERED_FD leftover fd is *
&(leftover
dropUntilIncl P (DROP pos (MAP (... ... ) content))
(pos STRLEN content
pos + LENGTH leftover + LENGTH (... ... (... ... ))
STRLEN content)))
failed.
Failed to prove theorem b_inputUntil_aux_spec.
Uncaught exception: HOL_ERR {message = "rewr_head_conv (THEN1 on line 4798) (THEN1 on line 4802) (THEN1 on line 5036) (THEN1 on line 4795) (THEN1 on line 4781) (THEN1 on line 5084) (THEN1 on line 4779) (THEN1 on line 5097)", origin_function = "failwith", origin_structure = "??"}