[isabelle] Sledgehammer and Nitpick from the command line?
- To: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Sledgehammer and Nitpick from the command line?
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Wed, 25 Jul 2012 21:19:26 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and