[isabelle-dev] I will start to fix my broken entries in afp-devel now

[Peter Lammich]

So if anyone else currently working on that, please tell me

Best,
  Peter

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] More SPASS with Isabelle

[Jasmin Blanchette]

Hi all,

The automatic prover SPASS, integrated in Sledgehammer, now includes many 
enhancements, such as properly oriented term simplification, that should make a 
difference for Isabelle problems. Thanks to these, SPASS has become more 
effective than E, Vampire, or Z3 [1], and this is just the beginning.

If you are using the latest development version of Isabelle and would like to 
try it out, simply follow these instructions:

1. Get the SPASS binary from

   Linux: http://www21.in.tum.de/~blanchet/spass-linux/SPASS
   Mac: http://www21.in.tum.de/~blanchet/spass-darwin/SPASS

   and put it somewhere (e.g., in /foo/bar).

2. Add the following line to your ~/.isabelle/etc/settings file:

   SPASS_NEW_HOME=/foo/bar

That's all. When you restart PIDE or Proof General and try Sledgehammer, 
spass_new will be one of the provers used by default. (The naming convention 
is temporary; once it has left the experimental stage, it will be called 
spass and subsume the old SPASS 3.7.) To test that it works fine, try

lemma rev [q,w,e,r,t,y,u,i,p,a,s,d,f,g,h,j,k,l,z,x,c,v,b,n,m] =
   [m,n,b,v,c,x,z,l,k,j,h,g,f,d,s,a,p,i,u,y,t,r,e,w,q]
sledgehammer [preplay_timeout = 0]

and see if spass_new finds a proof really quick.

I would be very interested in getting feedback from users, to see whether the 
new SPASS makes a real difference in practice.

[1] http://www4.in.tum.de/~blanchet/more-spass.pdf

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle/jEdit and Toplevel.debug

[Makarius]

On Sat, 11 Feb 2012, Florian Haftmann wrote:


In plain old tty days one would get a traceback for exceptions atfer

ML {* Toplevel.debug := true *}

Is this trace somehow accessible by jEdit also?


It is on the same low-level stdout channel as on the TTY or Proof General, 
but this is also the reason why it is less accessible in the Prover IDE -- 
due to lack of Isabelle/Isar transaction context.


Isabelle/jEdit provides a Raw Output panel for such physical process 
output, which is a bit awkward but not more than going back to TTY.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev