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