The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,

2009/4/21 Gyesik Lee 
<gslee AT ropas.snu.ac.kr>:
>...
> 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)"

As MAkarius said, it is probably due to your old version of emacs.
This may be a problem because it suggests some part of PG files are
not loaded. Since PG seems to work, it must be a small part. Please
consider submit a bug report on
http://proofgeneral.inf.ed.ac.uk/trac/wiki.

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

Yes it is. As there is no compatibilty problem between coq-8.1 and
coq-8.2, we did not add a specific v8.2 mode.  The message is an
information message for people dealing with several versions of coq at
the same time (pg guesses coq version by running coqtop -v and falls
in default mode if this fails).

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

This is the right way to install PG.

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

This is a bit old as Makarius said. On debian, I think emacs22 can
co-exist with emacs21 with no pain.


Regards
Pierre Courtieu