The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Any chance of a patch or plugin that works with 8.4?

-Jason

On Jun 6, 2014 9:50 PM, "Pierre-Marie Pédrot" <pierre-marie.pedrot AT inria.fr> wrote:

On 06/06/2014 20:33, Jason Gross wrote:
> Currently, [Timeout] raises an anomaly about sys.signal on Windows.  I may
> try my hand at writing a simpler variant as a plugin, but I figured I'd ask
> if anyone has already written something like this:
> How hard would it be to write the following variant of [Timeout], say,
> called [PoorMansTimeout n tac]: It would executes [tac] fully, measuring
> how long it takes, and is equivalent to [fail "Timeout!"] if it takes
> longer than [n] seconds, and is equivalent to [tac] otherwise.

I think we may instead use threads to mimic the timeout behaviour on
Windows. There is already a direct way to interrupt the process by
setting the Util.interrupt flag to [true]. I am going to write a patch
to test this.

PMP