Email Gateway (Aug 19 2022 at 16:27): Email Gateway (Aug 19 2022 at 16:27):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Marco,
I am currently removing smt from a lot of Isabelle proofs, and I noticed, strictly empirically, what follows.
A number of such proofs kept working by merely (and manually) replacing "by smt" (or "by smt2") with something like "by (metis(no_types,lifting))", (or metis with other combinations of options (e.g., hide_lams, mono_tags, etc...)).
I think that it would be nice, given the licensing issues, that sledgehammer would suggest these alternatives, rather than (or at least in addition to) "by smt".
By default, "smt" calls are only proposed if all else failed. More precisely, whenever Sledgehammer gives a "by (smt ...)", it's because the variations of "metis" failed or timed out. So if you successfully replaced "by smt" by something like "by (metis (no_types, lifting) ...)", it's either because it timed out or because the specific combination of "metis" options wasn't tried. (Those that are tried can be seen by passing "[verbose]" or "[debug]".)
However, I couldn't find a way of influencing s/h behaviour in such a way, by reading s/h manual.
I tried with smt_proofs=false, to no avail.
Well setting "smt_proofs=false" surely must have changed something, namely that you never get any "smt(2)" proofs, right? If not, that's really a bug, and I would like you to send me an example that reproduces the problem.
Already in Isabelle2014, Sledgehammer should attempt to generate Isar proofs (cf. "isar_proofs" option in the manual) for Z3 when offering "by (smt2 ...)". This support has been improved further in the repository version and should help you produce "smt(2)"-free proofs, fit for the AFP.
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 16:27):From: marco caminati <marco.caminati@yahoo.it>
Ven 21/11/14, Jasmin Christian Blanchette <jasmin.blanchette@gmail.com> ha scritto:
Hi Marco,
By default, "smt" calls are only proposed if all else failed. More precisely,
whenever Sledgehammer gives a "by (smt ...)",
it's because the variations of "metis" failed
or timed out. So if you successfully replaced "by
smt" by something like "by (metis (no_types,
lifting) ...)", it's either because it timed out or
because the specific combination of "metis" options wasn't tried.
The specific combinations usually take less then a second once I manually enter them, hence I think it's the second case.
Given that, I find that it would be nice if sledgehammer would try those combinations, too.
Of course I have no clue about whether this is technically possible.
(Those that are tried can be seen by passing "[verbose]" or "[debug]".)
I think this is a useful suggestion; however, at the moment I cannot try it.
Well setting "smt_proofs=false" surely must have changed
something, namely that you never get any "smt(2)"
proofs, right?
Exactly, no bugs. I just hoped that using that setting would have helped emerging alternative metis combinations.
Already in
Isabelle2014, Sledgehammer should attempt to generate Isar
proofs (cf. "isar_proofs" option in the manual)
for Z3 when offering "by (smt2 ...)". This support
has been improved further in the repository version and
should help you produce "smt(2)"-free proofs, fit
for the AFP.
Yes, indeed a couple of Isar proofs generated by SH were readable, and I happily used them.
It was a very nice sensation, by the way :)
I mean, reading a proof that nobody wrote.
Regards,
Jasmin
Thank you for the answer!
Best,
Marco
PS: Please bear with the horrible quoting, my webmail interface sucks seriously.
Email Gateway (Aug 19 2022 at 16:29):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Marco,
Am 21.11.2014 um 22:12 schrieb marco caminati <marco.caminati@yahoo.it>:
The specific combinations usually take less then a second once I manually enter them, hence I think it's the second case.
Given that, I find that it would be nice if sledgehammer would try those combinations, too.
Of course I have no clue about whether this is technically possible.
It's technically possible but would put more of a burden on the user's patience. All in all, it's a matter of calibration, of trade-offs. The state you described is clearly suboptimal, but things have changed a lot in the past year or so.
So once you've upgraded to the repository version or the forthcoming Isabelle2015, keep an eye on proof reconstruction, and if you still feel things could be improved further, I would be happy to get your feedback. I have myself started using Isabelle and Sledgehammer (as opposed to developing it) and did notice a number of misfeatures, which I quickly resolved. I will still not claim that everything is perfect. ;)
Yes, indeed a couple of Isar proofs generated by SH were readable, and I happily used them.
It was a very nice sensation, by the way :)
I mean, reading a proof that nobody wrote.
Thanks for the feedback!!
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 16:37):From: marco caminati <marco.caminati@yahoo.it>
I am currently removing smt from a lot of Isabelle proofs, and I noticed, strictly empirically, what follows.
A number of such proofs kept working by merely (and manually) replacing "by smt" (or "by smt2") with something like "by (metis(no_types,lifting))", (or metis with other combinations of options (e.g., hide_lams, mono_tags, etc...)).
I think that it would be nice, given the licensing issues, that sledgehammer would suggest these alternatives, rather than (or at least in addition to) "by smt".
However, I couldn't find a way of influencing s/h behaviour in such a way, by reading s/h manual.
I tried with smt_proofs=false, to no avail.
Is there a way to attain this result?
Last updated: Apr 26 2024 at 04:17 UTC