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



On 22.04.2014 13:36, Lawrence Paulson wrote:
> The best overall approach to all such situations is to fix syntax errors as soon as they are flagged. If I am working on a proof and notice that processing power is being wasted processing some proof text down below, I delete or disable this material. Inserting “sorry” beforehand should always do the trick. Needless to say, your work isn't done until every “sorry” has been removed again.
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 ...




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