[isabelle-dev] Sledgehammer on Cygwin

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Apr 24 15:16:23 CEST 2012

Hi Makarius,

> There are still various open questions here.

I will look into this later today.

>  lemma "[a] = [b] ==> a = b" sledgehammer [provers = e]
>  Sledgehammer: "e" on goal
>  [a] = [b] ==> a = b
>  "e": The prover ran out of resources.
> Any clues?  How can one get more information from the external prover?

   sledgehammer [provers = e, verbose]

or the strictly more verbose

   sledgehammer [provers = e, debug]

often help. To get even more information, you can even pass "overlord" (sic):

   sledgehammer [provers = e, debug, overlord]

Then you get files called "prob_e_1" (E's input) and "prob_e_1_proof" (E's output) in your "~/.isabelle" directory. This is very thread-unsafe, but I find it extremely useful for debugging.

But it's on my radar. I tested the 23 April package's Sledgehammer on my Mac (Snow Leopard) this morning and it worked like a charm. I'll try to reproduce the issues on Cygwin now when I get a second.


More information about the isabelle-dev mailing list