Timeout on cryptol-remote-api?

[michaelabernardo]

Good morning!

Is there a way to timeout or kill a command running on cryptol-remote-api if it doesn't complete after a period of time? For example, if I was trying to run :prove on a number of proofs, but wanted cryptol-remote-api to stop and move on to the next proof if it took more than two minutes on any given proof. I've tried implementing a timeout through Python that kills the command on my script, but I think the server keeps spinning, at least for a time.

Thank you!

[pnwamk]

Unfortunately the python client and server do not have this feature yet -- I'm chatting with some folks here now about how we could most conveniently add both timeouts and interrupts to the interface. E.g., perhaps having an optional timeout keyword argument to the Python prove function (and any other SMT-reliant functions) will work nicely for most use cases and be easy to implement, while a more general ability to interrupt the server might take a little more engineering but could obviously handle more things and be more dynamic.

I'm exploring workarounds in the meantime to see if we can leverage the underlying timeout features some of the solvers have to get around the server not yet supporting it explicitly. If I find something that works I'll post it here. Experiments thus far have been unsuccessful =\

[pnwamk]

@michaelabernardo If you have any ideas/suggestions/preferences on what this feature would ideally look like from a user perspective please don't hesitate to share =)

[pnwamk]

It looks like the most straightforward way to address this issue is to properly expose the solver timeout option in the underlying library Cryptol uses on to interact with the various solvers (i.e., what4). Once that is done, it should be trivial to add an option to Cryptol and Cryptol's server & python client to let users customize timeout behavior as needed. I should have more info on how/when we can land some of these changes in the next couple of days.

More generally it would be nice to tweak the server so any request can be interrupted if there is a need to do so. This still needs further investigation to see what changes would be necessary.

[michaelabernardo]

That sounds great! I think it would be nice to have a more general way to interrupt the server in the future, but the solver timeout will be very useful, as well.

[pnwamk]

Implementing proper interrupt handling (and not just timeouts) will likely relate to work done to fix this issue as well: #1167

[pnwamk]

Merging of this PR will address the "timeout" aspect of this general problem: GaloisInc/what4#128
Planning to look into outright interruptibility in the server soon.

[RyanGlScott]

If I understand correctly, this issue has been resolved:

• Enhance timeout handling what4#128 adds support for timeouts
• feat: server can now be interrupted, cancelling all active requests argo#174 adds support for interruptibility

Both of these are now in use in cryptol, so I'll close this.