REPL evaluation doesn't work after interrupting prover with Ctrl-C

[brianhuffman]

This seems very closely related to #1157. Since #1158, cryptol can continue gracefully after a Ctrl-C during evaluation or while waiting for input. But the REPL still gets into a bad state if you interrupt it during a long-running :prove command. This example reliably causes a "resource vanished" error for me on MacOS:

Cryptol> :prove \(x:Z 257) -> x^^257 == x
^C
SBV exception:

*** Data.SBV: Interrupt:
***
***    Sent      : (check-sat)
***
***    Executable: /Users/huffman/.bin/z3
***    Options   : -nw -in -smt2

Cryptol> True
cryptol: fd:13: hFlush: resource vanished (Broken pipe)

[robdockins]

I guess we need to be more clever about restarting the type-checking solver. Bummer, that's going to be a bit trickier.

[kquick]

This maybe related to something I'm working on right now in What4, where solver cleanup doesn't handle a closed solver process; I'll update this issue once I've completed that work to determine if that affects this issue.

[kquick]

There is a typechecking solver session running alongside that may be the issue. There is supposed to be code to restart this as needed, but perhaps that is not working correctly. Consider maybe starting the solver in a different process group, checking the ctlc_delegate flag, verifying cleanup actions aren't attempted after the process exits, and catching the exception.

[brianhuffman]

An acceptable behavior would be for Ctrl-C to cause all external prover processes to be killed and restarted.

[robdockins]

Just to add some color to this, I expected that https://github.com/GaloisInc/cryptol/commit/a45072dcb4e7c6de2f4706afa14cf7ec8c14d63a would basically do what Brian is asking for here (reset the solver on Ctrl-C). I don't understand why this handler isn't being called in this instance.

[yav]

This is a bit old, but I am adding the link here in case it contains something relevant: http://neilmitchell.blogspot.com/2015/05/handling-control-c-in-haskell.html

[robdockins]

Whelp, CTRL^C now appears to drop you out of the REPL altogether. I haven't checked yet, but I suspect this follows the merge of #1225.

[yav]

@robdockins what did you do exactly? I can't seem to get ctrl-c to do anything odd, at least on my Linux machine running bash. I tried ctrl-c directly at the REPL, while proving, and while evaluating.

I wonder if there is a platform specific difference we are encountering.

[robdockins]

I stopped a computation during a :prove, but while cryptol was still doing symbolic simulation before sending the problem to the solver.

I guess it could be platform-specific differences... sigh

[robdockins]

A little testing demonstrates that it only seems to happen when w4-offline is set as the prover... so maybe it isn't related to #1225 after all. I wonder what's different about that code path.