Hi, 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). Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
