[isabelle] isatool wanted by proofgeneral?
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and