both Proof General and Coq install and provide Emacs files and
features for 'coq, 'coq-db and 'coq-syntax (the latter two are
actually old versions from Proof General).

This is going to be a problem for those that want to use a
manually installed Coq 8.4 with a Debian installation of Proof
General. In Debian, manually installed stuff has precedence, so
when proof-site requires 'coq, Emacs will actually load coq.el
from the Coq installation. 

Note that the current Proof General package (version
4.2~pre120411-2) does suffer, because it violates the Debian
policy, see
http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=670339 . But
this will change soon.

Further, whole distributions (like Debian) where Proof General
and Coq are installed from packages are likely to ignore the
problem, because in ascii order "coq" appears before
"proofgeneral", therefore Proof General appears before Coq in the
load path. In such a installation only those who load
coq-inferior will have a problem, because the (require 'coq)
inside coq-inferior.el will load coq.el from Proof General.

One could of course argue that the problem should be solved by
those who mix a packaged Proof General with a manual install of
Coq. Or by those who designed Emacs with a flat namespace for
features and library files...

However, I believe it would be better if Coq and Proof General
use different feature names. Because I have the impression, the
Emacs mode distributed with Coq is rarely used, I would suggest
that Coq changes the names of 'coq, 'coq-db and 'coq-syntax. Or
supresses the installation of these files with the default 
"make install". 

If this is not going to work out, I would suggest that Proof
General changes file names (hoping that not more files are copied
from Proof General to Coq).


ProofGeneral-devel mailing list

Reply via email to