Email Gateway (Aug 18 2022 at 09:49): Email Gateway (Aug 18 2022 at 09:49):From: clinton lefort <ipub@charter.net>
Hello,
I am a newbie to Isabelle. I am trying to run my first program,
perhaps just an example file under Xemacs or Emacs.app I have a
macintosh and have downloaded all the files I need to get running,
but I have not been able to configure my files correctly. Could
someone help me with this? Below is a configuration of my files.
/user/clintonlefort/Isabelle_26-Sep-2006 Folder/Isabelle_26-Sept-2006/
ProofGeneral-3.5 Folder/ProofGeneral-3.5/bin/proofgeneral
Thank you for any suggestions how I can better configure my system
and get Isabelle to run. About a month ago I had it running, but
misplaced the configuration I had.
Clint LeFort
Email Gateway (Aug 18 2022 at 09:49):From: Elsa L Gunter <egunter@cs.uiuc.edu>
Dear Clint LeFort,
I too am a Mac user, and I had trouble getting Proof General working
under XEmacs. However, I was able to get it working properly under the
X11 version of Gnu Emacs 21.2.1. If you do get Isabelle working with
XEmacs, I would be interested in the details. If you would like to try
the Gnu Emacs version, I would be willing to give you a hand.
---Elsa L. Gunter (Elsa)
clinton lefort wrote:
Email Gateway (Aug 18 2022 at 09:49):From: Lawrence Paulson <lp15@cam.ac.uk>
I compile XEmacs using Fink, see http://fink.sourceforge.net/
Just install the packages "xemacs" and "xemacs-sumo-pkg". It isn't
difficult using the GUI, FinkCommander.
From time to time I have had big problems with XEmacs, but it has
been OK for me in the past year or two.
Larry
Email Gateway (Aug 18 2022 at 09:50):From: John Ridgway <jridgway@wesleyan.edu>
I use ProofGeneral, XEmacs, and Isabelle all the time. I get XEmacs
from MacPorts (formerly DarwinPorts), make sure you install the sumo
and mule variants. If you've already got MacPorts installed then all
you need to do is issue the following:
sudo port selfupdate
sudo port sync
sudo port install xemacs +sumo +mule
You need the sync step because mule support was only recently added.
See the MacPorts site http://www.macports.org/ for more information
on MacPorts.
BTW, you need to unpack ProofGeneral in the same directory as
Isabelle. My /usr/local looks like this:
Isabelle@
Isabelle2005/
ProofGeneral@
ProofGeneral-3.6pre060214
polyml@
polyml-4.1.3/
proofs/
Peace
Email Gateway (Aug 18 2022 at 09:50):From: David Aspinall <da@inf.ed.ac.uk>
Larry didn't mention his useful page on getting Isabelle and Proof
General running on Macs, here:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/macosx.html
I stole the PG part of this and put it onto the Proof General Wiki:
http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsOnMacOSX
I've added a bit more about native Emacs ports: I've been using
Carbon Emacs for a while, it works pretty well and looks pretty
(antialised fonts!). The main problem for Isabelle is the lack of X-
Symbol, but actually I don't think this is too difficult to fix. A
while ago I had a try, and I've put some notes now onto the Wiki
which describe what I did:
http://proofgeneral.inf.ed.ac.uk/wiki/Main/XSymbolOnMacOSX
Someone who has a bit of time (and a penchant for font formats) could
get things working along any of the three lines I describe. The
second and third solutions would not be just for Mac: Carbon Emacs is
based on the future Unicode based version of GNU Emacs which supports
rendering using Xft. It seems to work reasonably reliably on Linux,
but you have to build it yourself from CVS.
- David.
Last updated: May 03 2024 at 12:27 UTC