Re: [isabelle] Sledgehammer and Nitpick from the command line?
On 7/26/2012 2:56 PM, Makarius wrote:
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.
Okay. I'll keep that in mind, though it's not obvious to me right now
how I'm supposed to use that information to create a batch/bash file to
My idea right now is to use i3p. I used it a little in the past, and it
seems to be more of a light weight IDE. I can call it directly with a
batch file, unlike Proof General under Cygwin. I would have to manually
start the proving with i3p, but that's okay.
If I really get serious about testing theorems then I'll set up a true
Linux install on a quad core desktop that I'm not using.
This archive was generated by a fusion of
Pipermail (Mailman edition) and