Re: [isabelle] [Sledgehammer]



Dear Jasmin,

Again, many thanks for your reply.

I've attached two screenshots to visualize this situation exactly as it
arrives to me.

In the first one, you can see that the solution proposed by Sledgehammer
doesn't finish the proof ("by fastforce" is in purple and Isabelle
continues to show the goal).

The second screenshot is the situation, I described before.

The code for this theory is open source and can be found on its github
repository inside Cycles.thy theory:
https://github.com/DeVilhena-Paulo/GaloisCVC4/blob/master/Cycles.thy. The
line numbers for these situations can be read in the screenshots.

To repeat the first situation, click on apply Sledgehammer right after
?thesis. To repeat the second, write "using less" right after ?thesis and
apply Sledgehammer.

Cheers,

Paulo.

On Wed, May 2, 2018 at 12:26 PM, Blanchette, J.C. <j.c.blanchette at vu.nl>
wrote:

> Dear Paulo,
>
> I just reread your original email. Somehow I had misparsed "without" as
> "with"; hence the confusion. Sorry about that.
>
> > It just feels awkward that, for me, most of the time when this behavior
> appears is in very simple situations where the argument of performance
> wouldn't work at an intuitive level (I don't know the inner functioning of
> Sledgehammer, I'm simply based on the size of the one-line proof output as
> an user naively does). For example, there was a situation where all the
> provers outputed "by blast" and Isabelle wasn't able to finish the proof
> with this command.
>
> If Sledgehammer told you "by blast (10 ms)" or something like that and
> "blast" failed, this is a bug, and I would be interested in a
> self-contained example that reproduces the issue.
>
> > Another example, to make things concrete, was the situation of
> yesterday: if I write "using less" to give Sledgehammer a hint, all the
> provers but one proposed "empty by auto" as solution, which failed, and the
> last proposed "cycle_decomp.simps by auto" and also failed.
>
> If Sledgehammer told you, say, "by auto (20 ms)" and it failed, this is a
> bug.
>
> If you can send me a few examples and clear instructions on how to
> reproduce the problem, I could look into this. Please, however, disable
> machine learning, as it introduces some noise -- e.g. add
> "sledgehammer_params [mepo]" at the top of your file.
>
> Cheers,
>
> Jasmin
>
>

Attachment: Screenshot1 from 2018-05-02 12-47-17.png
Description: PNG image

Attachment: Screenshot2 from 2018-05-02 12-47-52.png
Description: PNG image



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