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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
