Put autodetected coq version in modeline?

[SkySkimmer]

This would be nice for people who switch somewhat frequently between versions.

This patch seems to work but IDK if it's the right way to do things

modified   coq/coq-mode.el
@@ -188,8 +188,10 @@ Near here means PT is either inside or just aside of a comment."
 (defalias 'coq--parent-mode
   (if coq-use-pg 'proof-mode 'prog-mode))
 
+(defvar coq-mode-line-version "")
+
 ;;;###autoload
-(define-derived-mode coq-mode coq--parent-mode "Coq"
+(define-derived-mode coq-mode coq--parent-mode `("Coq" coq-mode-line-version)
   "Major mode for Coq scripts.
 
 \\{coq-mode-map}"
modified   coq/coq-system.el
@@ -162,6 +162,7 @@ Interactively (with INTERACTIVE-P), show that number."
     (when mtch
       (setq coq-autodetected-version (match-string 1 str))))
   (when interactive-p (coq-show-version))
+  (setq coq-mode-line-version coq-autodetected-version)
   coq-autodetected-version)
 
 (defun coq-autodetect-help (&optional _interactive-p)

[erikmd]

Hi @SkySkimmer,

I believe you could be interested in https://github.com/ProofGeneral/opam-switch-mode ?

Indeed, the current opam switch is displayed in the modeline, e.g. opam switch system → OPSW-system

[erikmd]

BTW, @SkySkimmer, feel free to repost this old announcement https://discuss.ocaml.org/t/ann-release-opam-switch-mode-1-7-with-tuareg-merlin-support/12703 in the Rocq discourse, if you feel this emacs feature for ocaml+rocq is not visible enough.

[SkySkimmer]

No, my opam switch isn't named based on the rocq version it may contain, and not all my rocqs are opam installed, so opam switch name is useless to me.

[Matafou]

This would definitely be nice for users that compile coq by themselves.