[isabelle-dev] Sledgehammer on Cygwin
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Tue Apr 24 15:16:23 CEST 2012
> 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