[isabelle-dev] Total failure of sledgehammer

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Sep 12 23:43:08 CEST 2013

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

    lemma "hd [x] = x"
    sledgehammer (hd.simps)

2. If step 1 works, please try

    sledgehammer [mepo]


3. If step 2 works, please try


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.



More information about the isabelle-dev mailing list