Email Gateway (Aug 19 2022 at 10:40): Email Gateway (Aug 19 2022 at 10:40):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear all,
I learned about the "try" and "try0" tools to search for proof methods.
Now I wonder what's the right way of using them.
When "try0" says that, e.g. "by fastforce" is the fastest way to prove
something, does this automatically mean that I should _use_ "by
fastforce"? Or are there hidden traps?
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?
Thanks in advance for your help,
Christoph
Email Gateway (Aug 19 2022 at 10:41):From: Lars Noschinski <noschinl@in.tum.de>
On 08.03.2013 00:07, Christoph LANGE wrote:
I learned about the "try" and "try0" tools to search for proof methods.
Now I wonder what's the right way of using them.
Some of the proof methods in Isabelle are pretty similar on a higher
level, but have different strengths (in particular
auto/fastforce/force). try0 was invented so that one does not need to
try all the different calls by hand.
Reporting the timing is only a nice side effect, so one can easily
distinguish fast and slow proofs, not necessarily find "the fastest".
When "try0" says that, e.g. "by fastforce" is the fastest way to prove
something, does this automatically mean that I should _use_ "by
fastforce"? Or are there hidden traps?
Using "by fastforce" in this case is perfectly fine. Keep in mind that
the timings may vary.
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.
-- Lars
Email Gateway (Aug 19 2022 at 10:41):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Am 08.03.2013 um 08:14 schrieb Lars Noschinski <noschinl@in.tum.de>:
When "try0" says that, e.g. "by fastforce" is the fastest way to prove
something, does this automatically mean that I should _use_ "by
fastforce"? Or are there hidden traps?Using "by fastforce" in this case is perfectly fine. Keep in mind that the timings may vary.
I should add that the timings can be off, since we're using threads intensively. Sometimes it says 11 ms for blast and 12 ms for auto when the actual numbers are more like 1 ms for blast and 2 ms for auto. Take these timings with a grain of salt, as upper bounds.
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.
Jasmin
Email Gateway (Aug 19 2022 at 10:41):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 10:41):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 19 2022 at 10:43):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Gottfried,
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"
I think that's what it is. I'm still using Proof General, and there it's activated by going to "Isabelle > Settings > Global Timing".
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.
I don't know what the feature looks like in jEdit.
This helps a lot. Is there something special I'm supposed to be doing to use it?
I don't know. I use it if I want a background theory to load faster, to find out whether "blast" or "simp" is best.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 10:43):From: Lars Noschinski <noschinl@in.tum.de>
In jEdit you will get somehow unpredictable behaviour, as
Toplevel.timing is global state. In particular, there is no clean way to
disable it.
-- Lars
Last updated: Apr 23 2024 at 08:19 UTC