Re: [isabelle] isatool wanted by proofgeneral?

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.


(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:
On Sun, 17 Jan 2010, Elsa L Gunter wrote:

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

"Please give the full path to `isatool' (RET if you don't have it): <cwd>"

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).


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