The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Dear Peter,

You can ask Proof General about that:
M-x coq-show-version
or
M-x coq-autodetect-version

Best,
Anton

> On 8 Apr 2021, at 20:29, Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com> 
> 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.
> 
>