Email Gateway (Aug 18 2022 at 14:30): Email Gateway (Aug 18 2022 at 14:30):From: Elsa L Gunter <egunter@cs.uiuc.edu>
I am attempting to install Isabelle on two Linux systems, and I am
running into trouble. Both systems are running Emacs 21.4.1. I have
full control over one of the systems, but very limited control over the
other (it is a server or general student use). I have downloaded
polyml-5.3.0.tar.gz, ProofGeneral-3.7.1.1.tar.gz,
Isabelle2009-1_bundle.tar.gz, and HOL_x86-linux.tar.gz and unpacked then
into a local directory. I have added the (load-file
"<proofgeneral_home>/generic/proof-site.el") line to my .emacs file.
When I go to start up Isabelle by
isabelle emacs
it gets into loading Proof General, but then stalls, claiming "File mode
specification error: (void-variable image-load-path)". When I try
starting up emacs and then visiting a file, say tmp.thy, again it
proceeds to start loading Proof General, but then in the mini-buffer it asks
"Please give the full path to `isatool' (RET if you don't have it): <cwd>"
At first I was attempting to load Isabelle onto the student server, onto
which I had loaded previous versions. I assumed that I must have left
some trace of the old version and had some path set incorrectly
somewhere. But the problem persisted even after I had deleted all old
files. So I tried doing the installation on a machine that had just
been freshly loaded with a fairly generic linux and had never had
Isabelle on it, and the problem appeared there as well, with exactly the
same behavior. I have tried looking through the ProofGeneral files,
including interface and interface-setup.el and I cannot find the source
of the problem. I know that Emacs 22.2.1 is the preferred version of
Emacs, but the COMPATIBILITY file does indicate the Emacs 21.4.1 should
work with poorer support for X-Symbol sub/superscripts. I have used
Emacs 21.4.1 with acceptable results before. I would appreciate help in
trying to get Isabelle working again with it.
---Elsa
Email Gateway (Aug 18 2022 at 14:30):From: Makarius <makarius@sketis.net>
When using the regular "isabelle emacs" wrapper, their is no need to load
proof-site.el manually, and doing so might cause the problem (there might
be other reasons).
Makarius
Email Gateway (Aug 18 2022 at 14:30):From: Elsa L Gunter <egunter@cs.uiuc.edu>
Just to be sure, I have commented out the load-file line from my .emacs
file, and when I run isabelle emacs there is no change in behavior, as
indeed some examination of the scripts would indicate there shouldn't be.
On both machines I was installing a totally fresh copy of
Isabelle-2009-1. There is no other isabelle anywhere on either of these
machines. On one of them there never has been any other copy of Isabelle.
I've done a bit of further investigation and found that all of the code
referring to isatool is located in
ProofGeneral/isar/interface-setup.el. However, as cursory inspection
seemed to indicate that this file was the same as the one bundled in
the mac distribution, with which I have no problem. Therefore, I assume
my problem involves something more.
I have included below the Messages log from starting up isabelle emacs
on a totally generic linux box, in case it might be of assistance to
anyone who might be able to help me.
---Elsa
(emacs -l
/usr/local/Isabelle2009-1/contrib/ProofGeneral/isar/interface-setup.el
-l /usr/local/Isabelle2009-1/etc/isar-keywords.el -l
/usr/local/Isabelle2009-1/etc/proofgeneral-settings.el Scratch.thy)
Loading disp-table...done
Loading tool-bar...done
Loading image...done
Loading tooltip...done
Loading /usr/share/emacs/site-lisp/site-start.d/igrep-init.el
(source)...done
Loading
/usr/share/emacs/site-lisp/site-start.d/lang-coding-systems-init.el
(source)...
Loading encoded-kb...done
Loading
/usr/share/emacs/site-lisp/site-start.d/lang-coding-systems-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/python-mode-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/tramp-init.el
(source)...done
Loading time...done
Loading mwheel...done
Loading jka-compr...done
For information about the GNU Project and its goals, type C-h C-p.
Loading cus-edit...
Loading easymenu...done
Loading cus-edit...done
Loading
/usr/local/Isabelle2009-1/contrib/ProofGeneral/generic/proof-site.el
(source)...done
File not found and directory write-protected
Loading /usr/libexec/emacs/21.4/x86_64-redhat-linux-gnu/fns-21.4.1-x.el
(source)...done
Loading easy-mmode...done
Loading regexp-opt...done
Loading isar (source)...
Loading proof-splash (source)...done
Loading cl-extra...done
Loading cl-seq...done
Loading cl-macs...done
Loading derived...done
Loading isar (source)...done
Loading proof-script (source)...
Loading proof-menu (source)...done
Loading proof-script (source)...done
Loading proof-toolbar (source)...done
File mode specification error: (void-variable image-load-path)
Makarius wrote:
Last updated: Oct 31 2025 at 12:44 UTC