The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

At the very beginning of the *coq* buffer there should be a "welcome to coq" 
message which may have the information you want.

Gaëtan Gilbert

On 08/04/2021 19:29, Peter LeFanu Lumsdaine wrote:
> 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.