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.


	Makarius





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