The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

> Try to add:
>
> (setq coq-version-is-V8-1 t)

O.k. now a strange thing happens.

At starting up using "emacs test.v", it ends up with the following
message in the command line of emacs (v. 21.4) in the buffer "test.v".

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

while PG is not activated.

In the "Message" buffer, I can find the following:

==============
...
Loading /home/gslee/ProofGeneral-3.7.1/generic/proof-site.el (source)...done
Loading /usr/lib/emacs/21.4/i386-linux/fns-21.4.1-x.el (source)...done
Loading easy-mmode...done
Loadding coq (source)...
Loading proof-splash (source)...done
Loading cus-edit...done
proofgeneral is in coq8.1 mode (to force another version, see for
example C-h v 'coq-version-is-V8-0)'
Coq default abbrevs loaded
...

==============

It seems that PG is  but activated, but not compatible with Coq 8.2.1. (??)
(Coq is installed without using any option, i.e., just installed in
/usr/local/bin/.)
However when I try to open another Coq file using C-x C-f, then
suddenly PG is there and everything is fine.

The same phenomenon occurs every time when I start emacs.

> This is probably just one of the usual Proof General + Emacs 
> incompatibilities, and Coq is innocent.  (The same happens for Isabelle 
> Proof General all the time.)

Probably Makarius is right.
However there are some reasons not to touch the Emacs installation for
the moment.
(It is installed on a Debian linux server of a team, and many people
including the boss are happy with it.)
Indeed I have no problem with the following combination:

Mac Leopard + Aquamacs (newest version) + PG 3.7.1 + Coq 8.2.1

> It seems that debian package of PG is not well built. Did you try to 
> install ProofGeneral by hand please?
> Can you describe the problem more precisely please? And your installation? 
> Then we decide if this thread should migrate to PG list.

Yes I installed the tar file by hand. I just downloaded the tar file,
unpacked and saved, then added the following line to .emacs:

(load-file "~/ProofGeneral-3.7.1/generic/proof-site.el")

The Coq installation was very standard on a Debian linux server.
Emacs version is 21.4.1

> Anyway, which versions of Emacs work best for you on Mac OS?

For me, I am really happy with Aquamacs, better than Carbon Emacs.
Easy to install and update, and nice fonts. Maybe too much patchwork
compared to the original GNU Emacs, but I use only basic things.

Gyesik