The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

Dear all,

Is there a vernacular command that gives the version of the Coq process — i.e. prints similar info to what “coqtop --version” outputs, but which can be called inside a Coq session?  Alternatively, is there any command that gives the location of the currently active Coq executable, or something else from which the version can be robustly deduced?  I’ve searched through the manual a bit, but haven’t managed to find these.

(My use-case: I occasionally find myself in a Proof General session, but uncertain which copy/version of Coq has been invoked by Emacs/Proof General.  Of course, one can easily check what command Proof General issued to invoke it, but Emacs often has a different $PATH from the ambient system, and other such issues, so it can take several surprisingly non-trivial steps to figure out precisely which version it’s invoked.  I’m sure for serious emacs people this is second nature, but I find it quite tricky each time, so I hoped there might be a vernacular command “Print Version.” or similar.)

Best,

–Peter.