Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabella proof general


view this post on Zulip Email Gateway (Aug 18 2022 at 14:13):

From: Aparna G <aparna_g@ymail.com>
When i try to use isabelle through Xemacs,it givs following error:
13 [main] xemacs 5380 child_copy:linked dll data write copy failed,win 32 error 487.

I am not able to understand how i can solve proofs as i am unable to get the theorem solving options... Any advice or help at earliest wud be great!

view this post on Zulip Email Gateway (Aug 18 2022 at 14:13):

From: Makarius <makarius@sketis.net>
This sounds like some of the usual Emacs problems that happen
occasionally. Instead of fiddling with Windows and Cygwin, you might also
consider install Linux on your machine, e.g. see http://wubi-installer.org/

GNU Emacs 22 or 23 usually works best with Proof General, which is the
default Isabelle user interface that you are faced with.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 14:13):

From: Tim McKenzie <tjm1983@gmail.com>
I couldn't get X-Symbol to work in GNU Emacs 23, so I went back to
GNU Emacs 22. Have other people got it working in Emacs 23, or is
X-Symbol no longer preferred?

Tim
<><
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 14:13):

From: Lucas Dixon <ldixon@inf.ed.ac.uk>
X-symbols has been dropped from proof-general in emacs 23, in favor of
Unicode tokens. I use emacs 23.1, proof-general 4 beta cvs checkouts,
and development snapshots of Isabelle. But getting a working collection
of tools is pretty tricky. :(

For Isabelle 2009, I think the best combination is x-symbols and emacs
22. If you have afs filesystem access, you can see my setup of this at:

/afs/inf.ed.ac.uk/group/dreamers/public/software/Isa2009

See the file "source_me.sh", which sets up paths etc.
If you have a similar unix machine, you might even be able to run it
directly from there (probably slowly!).

But you can use that as a template for making your own local installation.

best,
lucas

Tim McKenzie wrote:

view this post on Zulip Email Gateway (Aug 18 2022 at 14:14):

From: Tim McKenzie <tjm1983@gmail.com>
Thanks; this is the setup I'm using at the moment. I was curious
to know whether it would be worth trying to get Emacs 23 working,
but it sounds like I should wait.

Tim
<><
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 14:15):

From: Sigurd Torkel Meldgaard <stm@cs.au.dk>
I am using 23 with Unicode-tokens, and it seems to work fine.

Sigurd.


Last updated: Apr 19 2024 at 04:17 UTC