Re: [isabelle] problem installing the necessary software for Isabelle2008



On Fri, 17 Oct 2008, Andrei Popescu wrote:

> Kubuntu (a version from 2006). 
> Emacs 21.4.1.

> I followed the instructions from the website, but I get the following 
> error when I try to run Isabelle from ProofGeneral, as "Isabelle -p 
> emacs":

> File mode specification error: (void-variable image-load-path)

Even though that version of Emacs is a bit old, the COMPATIBILITY file of 
Proof General 3.7.1 says "tested; poorer X-Symbol sub/superscript 
support".  So it should work in principle.

Grepping through then elisp sources reveals the following line in 
proof-toolbar.el:

      (add-to-list 'image-load-path proof-images-directory) ; rude?

So you can try what happens without that.


Since GNU Emacs 21 is not so nice for Proof General anyway, you can also 
try to compile XEmacs 21.4.x yourself.  The main sources are available 
here:

  http://www.xemacs.org/Releases/index.html#Stable

You need to configure with MULE support.  Moreover the SUMO tarballs both 
for non-MULE and MULE are required, see 

  http://www.xemacs.org/Documentation/packageGuide.html#The_Sumo_Tarball


Yet another way to get a working Emacs for Proof General is to upgrade to 
a more recent version of Ubuntu and use the GNU Emacs 23 that is included.  
(The XEmacs package of Ubuntu is usually broken, due to its Debian 
heritage.)


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.