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
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:
smt e spass z3_tptp z3
theorem really_important_result_neg: "~(the Riemann conjecture is true)"
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and