Re: [isabelle] Problem with timeLimit



Thanks. Good to know that the problem is fixed. The current situation is quite acceptable for me. If the bug causes more problems, I will consider porting the fix to Isabelle2011.

-Matthias

Am 23.06.2011 11:45, schrieb Makarius:
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.