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 automate everything.

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.

Thanks,
GB








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