Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



On Tue, 22 Apr 2014, Lars Noschinski wrote:

What I sometimes wished for (in interactive mode) was a way to limit the resources (in particular cpu-time) consumed by the proof tools. I almost never write proofs where a single method call takes longer than a second; so a single proof method which takes more than say 10s is a sure indication of a broken proof (for me). But this is of course hard to codify in a robust and system-independent manner ...

Time limits indeed introduce erratic behaviour. Nonetheless, I have something like this on my list of further improvements of PIDE document processing for a long time. It might be even done in a manner of "iterative deepening", with 2-3 rounds of attempts to check some piece of text with increasing timeout. Doing that with a few milliseconds in the first round might even have a big impact on overall reactivity of the proof checking game, although that is pure speculation at the moment.


	Makarius




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