From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I've recently obtained Leopard, and the new version of Isabelle, and
have got it all set up, except that when I type /usr/local/bin/
Isabelle, it opens up in an X11 window rather than in XEmacs (but
proof general is already pre-loaded). XEmacs seems to work fine if
you start it on its own; I've downloaded the version, via macports,
which is suggested on the Isabelle website. On my old computer, I
had used the fink installer, which installed xemacs in
/sw/bin
whereas macports installs it in
/opt/local/bin
So, after it didn't work, I created a symlink in /sw/bin, and then
recompiled proofgeneral (I didn't know if this was necessary, but it
didn't seem to harm anything; afterwards it all worked to the same
standard as before, i.e. without XEmacs). I then tried editing the
makefile that comes with ProofGeneral, but this was less than
successful. Does anyone know if there is a variable in one of the
various settings files that I can set so that my installation knows
where XEmacs is?
Thanks
Peter
From: Francesco Librizzi <librizzi@dmi.unict.it>
Hi Peter,
I'm new with Isabelle, and last Friday I tried to install it for the
first time.
To obtain the XEmacs interface, I type:
/usr/bin/Isabelle/bin/isabelle-interface
If I type only isabelle, it run the X11 window.
I hope that my aid works for you.
bye,
Francesco
Il giorno 26/nov/07, alle ore 10:20, Peter Chapman ha scritto:
From: Lawrence Paulson <lp15@cam.ac.uk>
I don't understand how you can be runnning PG without XEmacs. Do you
mean it is in GNU emacs in an XTerm window? I didn't know that was
possible.
Anyway, when I installed Leopard, I noticed that MacPorts software no
longer worked. The simplest way to update your MacPorts setup
(especially if you only want XEmacs) is to delete /opt, then install a
fresh copy of Macports, and finally install XEmacs by
sudo port install xemacs +mule +sumo
If you have an old copy of /sw lying around, definitely delete that
first. It can't be wise to use Fink and Macports at the same time.
Larry Paulson
From: Lucas Dixon <ldixon@inf.ed.ac.uk>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
My last attempt to use Isabelle on a Mac (CVS snapshot of Isabelle, 2
weeks ago) resulted in me being happiest with Carbon Emacs (thanks to
David Aspinall for the suggestion), so I'd recommend that - it's a mac
native package, and you can install proof general for it easily (see
proof general webpage).
Don't know if other people have different experiences?
lucas
Lawrence Paulson wrote:
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFHS/QLogMqU4edHsMRApw+AJ0b8g1Ak2lyR108d/f5QnHxhmaHKwCghwgY
FbXFR41FfZSXfl+Izvrd4VE=
=qfQZ
-----END PGP SIGNATURE-----
From: Nicole Rauch <rauch@informatik.uni-kl.de>
Hello Lucas,
Does it support X-Symbol? There were some issues with X-Symbol not
being supported by some / all (?) of the native ports
(Aquamacs, ...), but I did not investigate too closely.
Cheers,
Nicole
From: David Aspinall <da@inf.ed.ac.uk>
Please see the PG Wiki for status/discussion:
http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsOnMacOSX
http://proofgeneral.inf.ed.ac.uk/wiki/Main/XSymbolOnMacOSX
Since writing that last year, the Stix fonts have been released (in
beta), and I've been shown how it it is possible to adjust character
baselines positions in GNU Emacs. So we are close to a good native
solution. I would welcome any help in getting there!
- David
Last updated: Nov 21 2024 at 12:39 UTC