Email Gateway (Aug 18 2022 at 09:45): Email Gateway (Aug 18 2022 at 09:45):From: Timothy Bourke <timbob@bigpond.com>
It turns out that there was just a misunderstanding about when the
Isabelle menu appears, i.e. not before opening a .thy buffer.
Tim (maintainer of FreeBSD port)
Email Gateway (Aug 18 2022 at 09:48):From: Tim Newsham <newsham@lava.net>
I installed Isabelle using the FreeBSD ports system. When I run
"proofgeneral" xemacs pops up with the proof general splash screen, but
there is no Isabelle menu (as described in the Isabelle tutorial).
Installing Isabelle caused the latest version of xemacs to be built and
installed. Does Isabelle have problems with new versions of XEmacs? Is
this a deficiency of the FreeBSD port of Isabelle? Am I doing something
wrong?
Tim Newsham
http://www.thenewsh.com/~newsham/
Email Gateway (Aug 18 2022 at 09:51):From: Makarius <makarius@sketis.net>
On Sun, 1 Oct 2006, Tim Newsham wrote:
Does Isabelle have problems with new versions of XEmacs?
Yes, more precisely this is a matter of the ProofGeneral + XEmacs
combination. Recent versions of the stable branch of XEmacs 21.4.14-19
should work, but many 21.5.x versions fail.
Is this a deficiency of the FreeBSD port of Isabelle?
Maybe. Experience shows that prepackaged OS packages for Isabelle +
Poly/ML + ProofGeneral cause more problems then they are meant to solve in
the first place. It is a good idea to try the plain tar.gz archives from
the Isabelle download site before venturing on ports, debs, rpms etc.
Unfortunately, XEmacs cannot be packaged as easily as the other
components, so you may have to recompile it from the orginal sources
(which works reasonably well if you just take all of XEmacs Mule + Sumo).
Makarius
Last updated: May 03 2024 at 12:27 UTC