Feature name conflict with Coq

[Hendrik Tews]

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

[Stefan Monnier]

Or by those who designed Emacs with a flat namespace for features and
library files...

Ahem!
Please don't put .../ProofGeneral/coq in the load-path, and then simply
do (require 'coq/coq).

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

Another take on it is that the two teams should join their efforts.


Stefan

[Pierre Courtieu]

Post by Stefan Monnier
Another take on it is that the two teams should join their efforts.

I already asked why this old file is still in coq distribution. The
answer was: some people just want to open coq file for syntax
highlighting. For them starting pg is too slow (+ splash screen).

I am ready to convince coq people to remove them if we can provide
some switch for a "light" PG loading where no scripting feature is
provided. In this case we could simply ask that that no emacs file
should be distributed with coq.

P.

[Hendrik Tews]

Post by Stefan Monnier
Another take on it is that the two teams should join their efforts.

I already asked why this old file is still in coq distribution. The
answer was: some people just want to open coq file for syntax
highlighting. For them starting pg is too slow (+ splash screen).

Is it just about the splash screen? It can be disabled easily
with proof-splash-enable. BTW, who wants to see the splash screen
on any Proof General start anyway? Don't get me wrong: I like the
splash screen and I am happy about its existence. Nevertheless,
the first thing that I configured for Proof General was
proof-splash-enable.

How about disabling the splash screen by default and enabling it
explicitly for those shell scripts that are called by menu items?

I did some measurements about startup times. Proof General needs
about 1.3 seconds until it is idling when starting form the shell
("emacs test.v"). The coq-mode from Coq needs about 0.9 seconds,
this _is_ noticeably faster.

Loading the generic part (proof-site.el) only takes 0.004 s, but
loading the prover specific part ((load-library ,elisp-file) in
the coq-mode stub takes 0.3 seconds. Then after the coq-mode
stubs finished, that is after the real coq-mode has been
finished, it takes another 0.3 seconds until emacs starts idling.
It is not clear to me, what it is doing in these last 0.3
seconds.

Bye,

Hendrik

[Hendrik Tews]

Or by those who designed Emacs with a flat namespace for features and
library files...

Ahem!
Please don't put .../ProofGeneral/coq in the load-path, and then simply
do (require 'coq/coq).

Where is this documented? I would even say that the Elisp manual
(sect 15.7)

If the feature is not present, then `require' loads FILENAME with
`load'. If FILENAME is not supplied, then the name of the symbol
FEATURE is used as the base file name to load.

implies that require 'coq/coq should load "coq\/coq.el" instead
of "coq.el" in subdir coq.

Bye,

Hendrik

[Hendrik Tews]

Hendrik Tews <tews-IG//nw+yl+***@public.gmane.org> writes:

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.

I only found out yesterday, that the load-path management is
severely broken in Debian (I would say), see bug #676424. So I am
not going to change the load-path management of Proof General now
and manual installs of Coq 8.4 are going to work as usual.

Nevertheless, we should try to solve the feature name conflicts.

Bye,

Hendrik