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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and