Re: [isabelle] Sledgehammer and Nitpick from the command line?



Being able to run Sledgehammer and Nitpick from batch/bash files would create lots of convenient possibilities.

It's not just about testing what you've proved. If had a new theorem I was about to start working on, then I could run a 30 second Sledgehammer and Nitpick test on both the theorem and its negation, which would be the 4 tests. I could then start 1 or 2 longer tests before starting my attempt to prove the theorem.

It would also conveniently allow me to run two different groups of provers independently on the same theorem in different console windows, the two groups being the local provers and the remote provers. It's good to get Sledgehammer to terminate normally, but you don't know when the remote provers are going to timeout.

I'm about to start an overnight experiment with the timeout set to 4 hours, but I want predictability, so I'm not going to put any of the remote provers in. I'd need to have two independent jEdit sessions running, like I talk about below, to not end up with a situation where the remote provers never come back, and Sledgehammer is still running 8 hours later.

Regards,
GB



On 7/25/2012 9:19 PM, Gottfried Barrow wrote:
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.