I've compiled and installed both cvc4 from source code. Cvc4 was downloaded and installed as suggested, and Cryptol was downloaded from it's git repository. The sandboxing, and installation finished without error (with GHC 7.8.3 x86_64). The issue occurs only after invoking cryptol, and issuing a :prove True. Here is everything:
athan@namek ~/lib> cryptol
_ _
___ _ __ _ _ _ __ | |_ ___ | |
/ __| '__| | | | '_ \| __/ _ \| |
| (__| | | |_| | |_) | || (_) | |
\___|_| \__, | .__/ \__\___/|_|
|___/|_| version 2.1.0 (8898348)
Loading module Cryptol
Cryptol> :prove True
cryptol: fd:6: hGetLine: end of file
athan@namek ~/lib>
Any help with this would be tremendous. To me, it feels like there's a shared library not found. Would that cause this issue? Thank you.
Summarizing the conversation in the comments:
The "end of file" error mentioned in the question is commonly attributed to the prover of interest (CVC4 in this case) being only "partially installed" - in my cases this was always an issue with shared libraries that could be discovered by invoking the binary (cvc, boolector, etc) from the command line. The ticket for the bug where the REPL would terminate is on Cryptol's github. Fortunately, this issue was fixed in upstream SBV and will appear in Cryptol's fork of SBV soon.
WRT AthanClark's particular case it is still unknown why and how CVC4 was failing when invoked by Cryptol - possibilities include cryptol invoking a different binary than the one we are expecting or environmental differences, such as the LD_LIBARARY path variable. Either way, it sounds like he was able to use an alternative prover (boolector) successfully.
EDIT: If you can produce Athan's bug, where CVC works outside of SBV and not inside of SBV... and you live in Portland then shoot me a message, show up at my office and show me, I'd be interested.