[isabelle-dev] Total failure of sledgehammer

[Lawrence Paulson]

None of them work.

I did enable MaSh.

The new Isabelle pre-release does work.

Larry

On 12 Sep 2013, at 22:43, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> Hi Larry,
> 
> Am 12.09.2013 um 20:14 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
> 
>> Provers don't launch at all (according to process monitor) and no output, either in the new S/H panel or via the sledgehammer command. I'm using 9d8764624487 but I don't think the precise version matters, as I grabbed a new copy this morning and nothing's changed.
>> 
>> Anybody else seen this?
> 
> I'm using the slightly more recent 3fb81ab13ea3 (but as you pointed out, hardly anything has changed in between) and everything is OK here. Let's try to debug this systematically.
> 
> 1. First, can you confirm that this total failure of Sledgehammer also occurs in the following example (which should be solved quasi instantly by several ATPs)?
> 
>    theory Scratch
>    imports Main
>    begin
> 
>    lemma "hd [x] = x"
>    sledgehammer (hd.simps)
> 
> 2. If step 1 works, please try
> 
>    sledgehammer [mepo]
> 
> instead.
> 
> 3. If step 2 works, please try
> 
>    sledgehammer
> 
> without any options.
> 
> 4. If step 3 works, try to construct a minimal self-contained example that doesn't work and send it to me.
> 
> One of my suspicions is that you might have enabled MaSh and today's change to it might have broken things somehow. Another  We'll definitely need to be more conservative in our changes getting closer to the release.
> 
> Thanks for your help.
> 
> Cheers,
> 
> Jasmin
>