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



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: http://pu.inf.uni-tuebingen.de/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.

DETAILS

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.

I attach a zip file with all the files, though I don't expect anyone to have time to pursue anything. I might think I'm wasting my time other than I'm figuring out what will start and terminate the prover processes.

Here is the theory with sledgehammer:

theory z0
imports z0i
begin
sledgehammer_params[verbose=true,isar_proof=false,timeout=120,provers="
  z3 e spass z3_tptp cvc3
  "]
theorem emS_is_unique_Sn:
  "~(\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS)"
  apply(auto)
  sledgehammer
  oops
end

Here is the file it imports:

theory z0i
imports Main
begin
typedecl --"The primitive set type: everything is a set."
  sT
consts --"Set membership predicate: to be axiomatized by subsequent axioms."
  inS::"sT \<Rightarrow> sT \<Rightarrow> bool" (infixl "IN" 55)
abbreviation
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."
  emS::sT
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)
end

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"

Regards,
GB










Attachment: 120726__sledge_with_usedir.zip
Description: Binary data



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