Configure maximum time

[jariji]

Currently I can set max_examples, but the actual constraint I want to impose is on the duration of the execution, and I don't know how long each example takes. So I would like to set a timeout (timeout, max_seconds, etc) on @check or in the config.

[Seelengrab]

This is something I definitely want to support! Unfortunately, there isn't a good way to cancel a Julia task (which is how this would be implemented) at the moment. A still-running computation might interfere with other code running at the same time, or just hog resources unnecessarily, even if @check has already continued its work. I don't really feel comfortable with letting tasks potentially dangle like that. As a consequence, the way I'd implement this at the moment would be to attempt a best-effort to stop after the timeout has passed and @check gets control again. This would mean that we potentially overrun the time budget, so the timeout wouldn't be "hard" in that sense.

There are also multiple durations a timeout could apply to:

• The entire invocation of @check
  • This case has lots of complications, depending on where exactly in the invocation the timeout occurs
    • If there's no counterexample, we can just report as Pass
• Only the "find a counterexample" phase
  • This would mean letting the shrinker run to completion, no matter whether we overrun the budget
• One individual example run
  • This could be useful for detecting unwanted long computations, and starting to shrink in the direction of "it still takes too long".

All of these have various consequences in regards to how "hard" the deadline implied by such a max_seconds configuration would be.