Pierre Courtieu <pierre.court...@cnam.fr> writes:

   2012/6/6 Stefan Monnier <monn...@iro.umontreal.ca>:
   > 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

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


ProofGeneral-devel mailing list

Reply via email to