Re: [isabelle] Recommended use of try and try0



On 3/8/2013 8:52 AM, Jasmin Christian Blanchette wrote:
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. Jasmin

Jasmin,

What is this "global timing"?

I know how to use "min" to check the timing of metis proofs, and I now see that try0 and try give some timing information. But how do I check the timing of proofs in general?

I found this in the mailing list archives:

    ML_command "Toplevel.timing := true"

When I put that in, the Isar commands have an orange line under them. If I hover over them, some give timing information, and some don't. If I change "by" to "apply", then I get timing information, but "by" by itself doesn't give any timing information.

This helps a lot. Is there something special I'm supposed to be doing to use it?

Thanks,
GB






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