The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature