Re: [isabelle] Sledgehammer and Nitpick from the command line?
On Wed, 25 Jul 2012, Gottfried Barrow wrote:
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.
Long-running IDE sessions do not make much sense. The tty or unattended
batch script are the right approach for that.
You need to take care that Isabelle/Scala/jEdit present a Unicode
rendering of the prover sources to you, so copy-paste into a plain
"isabelle tty" session will not work. You can use "Reload with Encoding"
in jEdit to use UTF8 instead of the default UTF8-Isabelle -- it will
reveal the true form of the prover in put sources that can then be copied
into the raw process. The latter might still cause additional problems on
Windows. It might require some experimentation with the Cygwin-Terminal
to see how it works.
This archive was generated by a fusion of
Pipermail (Mailman edition) and