Re: [isabelle] Recommended use of try and try0



On 08.03.2013 15:52, Jasmin Christian Blanchette wrote:
More generally, is it a recommended practice to occasionally revisit my
proofs, replace "by<some automated method>" by "try" everywhere, and
then generally use the proof methods that "try" recommends?

If you have a working proof which is robust and not too slow I don't see any need to revisit this proof.

If you have the feeling that your theory is processed slowly, you can spend some time doing that. I've achieved significant gains for Andrei Popescu and Dmitriy Traytel's formalization of cardinals, by turning on global timing and trying various things (often manually, sometimes with try0 or try). But if you're happy with the processing speed, there's no reason to bother.

Note that in jEdit you can already get timings for each command without changing any settings. However, there seems to be no nice interface yet:

In the Sidekick change the parser from "isabelle" to "isabelle-raw". If you now hover over commands in the Sidekick, you the see the answers from the prover in some XML format, including a "timing" element.

  -- Lars





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