[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 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






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