Re: [isabelle] Problem with timeLimit



On Thu, 23 Jun 2011, Matthias Schmalz wrote:

When evaluating "timeLimit time f x", I suspect that the "watchdog" sometimes interrupts the current thread after the evaluation of "(restore_attributes f) x"; the interrupt is then delayed (thanks to uninterruptible) until after the evaluation of "timeLimit time f x".

Yes, I had seen this before. Just after the Isabelle2011 release I've spent some time on it again, including in-depth discussion with David Matthews to understand the exact Poly/ML runtime behaviour here.

This resulted in the following changes http://isabelle.in.tum.de/repos/isabelle/log/2b92a6943915/src/Pure/Concurrent/time_limit.ML

It probably requires some fiddling to port this back to Isabelle2011.

You can also try Poly/ML 5.4.1-SVN, although it is still in flux. IIRC, David had some clarification there in his code as well, that demands less adjustment as I did for the official Poly/ML versions.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.