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