[isabelle] Sledgehammer and Nitpick from the command line?



I have a theorem that I want to test with Sledgehammer and Nitpick by calling isabelle from the command line.

For the Sledgehammer test, it's in a theory like this:

theory z0
imports z0i
begin
sledgehammer_params[verbose=true,isar_proof=true,timeout=10000000000,provers="
  smt e spass z3_tptp z3
  "]
theorem really_important_result_neg: "~(the Riemann conjecture is true)"
  apply(auto)
  sledgehammer
  oops
end

Is there a way to do this so that I get to see the Sledgehammer output?

I've broken a theory with 4 different tests into 4 different theories with one test each using Sledgehammer or Nitpick.

If they're all in one theory, then I have to run them sequentially. If I have 4 different theories, and I want to run them all at the same time, then I have to have 5 jEdit views open.

I probably don't want to be running 4 tests at the same time, but there's a good chance I at least want to run 2 at a time. Tests being what they are, I want to terminate them sometimes. Starting and terminating processes can mess up the one jEdit session that's managing all the views.

I could start up a completely independent jEdit session, other than they're not completely independent because they'll use the same home folder. Well, I could set the environment so they use different home folders.

Anyway, what I really want to do is run them all from the command line. If I'm testing the negation of a theorem that's been proved, then I'm not expecting Sledgehammer to prove the negation. I could start a test in a console window with an 8 hour timeout, and then work in jEdit independently, where I tend to start and shutdown jEdit quite a bit.

I looked at "isabelle tty" briefly, but that didn't look like the solution, though it may be. I searched in the Sledgehammer manual on "command", and I didn't find anything.

Thanks,
GB





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.