[isabelle-dev] Sledgehammer on Cygwin

[Jasmin Christian Blanchette]

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.

Jasmin