[isabelle-dev] Total failure of sledgehammer

[Jasmin Christian Blanchette]

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