[isabelle-dev] interrupts and timeouts

Makarius makarius at sketis.net
Tue Feb 8 18:10:59 CET 2011


In the past few months/weeks/days certain issues of interrupts and 
timeouts (which are based on interrupts internally) have emerged in 
private mail conversations with several people.

Recently David Matthews has kindly clarified some extreme corner cases, so 
I've made another round to robustify this on our side, e.g. see the 
vicinity of 82339c3fd74a.

There are still some pending questions concerning interactive "auto" 
checking tools, though.  I've first thought that this could be related, 
but the reasons might be much more profane.  (The above-mentioned corner 
cases of Poly/ML interrupts are so extreme, that they might not have shown 
up in practice so far.)


 	Makarius


More information about the isabelle-dev mailing list