Re: [isabelle] Sledgehammer and Nitpick from the command line?

(I sent this email in earlier today, but it never showed up on the list. The other had an attached zip file containing my experiment files, so that might have been why it got rejected.)

On 7/26/2012 4:36 AM, Jasmin Blanchette wrote:
The "system.pdf" manual explains how to process Isabelle theories on
the command line. I never remember the exact syntaxes and have to look
it up each time, but look for the "isabelle usedir" tool. (There might
be other tools as well.) This is nothing specific to Sledgehammer.
Regards, Jasmin

I tried that, but I'm doing something in a theory that you wouldn't normally do, which is leaving a sledgehammer command under a theorem, and wanting usedir to give me sledgehammer feedback like I get in jEdit. This would probably be a feature request, which I'm sure you don't have time for.

I'll try using i3p:

If I start sledgehammer in jEdit with a long timeout, I have to be careful not to disturb jEdit by scrolling around. Otherwise, it'll start sledgehammer again, new prover processes will get started, and old prover processes won't get terminated.

Here are some details if you have time. I can get a decent solution with either i3p, Proof General, or jEdit. All of them have some GUI overhead, and overhead from having multiple sessions running, but that's the cost of doing business. Part of the solution is to run these tests on a different computer.


If I use "usedir" on a theory which has a sledgehammer command in it, an eprover.exe process gets started (sometimes) that never gets terminated, and usedir gives some warning messages even though it finishes building the HTML, GraphBrowser.jar, and session.graph in the browser_info folder.

Further experimenting, I find out that what happens is not always the same. I'm using sledgehammer in a way it's not meant to be used, so what's happening is meaningless to some degree.

With five provers in, I get five warning messages like on the second line below:

Building z0 ...
sh: /cygdrive/e/Isabelle2012/contrib/exec_process-1.0/x86-cygwin/exec_process: Bad address

I take two provers out, and an exec_process.exe process gets started which never gets terminated. With sledgehammer only running "e" and "spass", an "eprover.exe" process gets started that never gets terminated.

With no sledgehammer command in, usedir work as expected.

Here is the theory with sledgehammer:

theory z0
imports z0i
  z3 e spass z3_tptp cvc3
theorem emS_is_unique_Sn:
  "~(\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS)"

Here is the file it imports:

theory z0i
imports Main
typedecl --"The primitive set type: everything is a set."
consts --"Set membership predicate: to be axiomatized by subsequent axioms."
  inS::"sT \<Rightarrow> sT \<Rightarrow> bool" (infixl "IN" 55)
ninS::"sT \<Rightarrow> sT \<Rightarrow> bool" (infixl "nIN" 55) where "x nIN y == \<not>(x IN y)"
consts --"The empty set: naively named as a constant."
axiomatization --"Axiom of existence: the empty set is empty." where
  eeA:"\<forall>x. \<not>(x IN emS)"
axiomatization --"Axiom of extention: set equality." where
exA: "\<forall>u. \<forall>v. (\<forall>x. x IN u \<longleftrightarrow> x IN v) \<longrightarrow> u = v"
theorem emS_is_unique --"The empty set is unique.":
  "\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS"
  by (metis eeA exA)

Here is ROOT.ML

  no_document use_thy "ThisTheory";
  use_thy "ThatTheory";
use_thy "z0";

Here is the usedir command:

    isabelle usedir -b HOL z0

Here are my usedir etc/settings

ISABELLE_USEDIR_OPTIONS="-i true -g true -M max -p 1 -q 2 -v true -V outline=/proof,/ML"


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