Automatically detect which version of Coq we're using

3 files changed, 67 insertions, 27 deletions

diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 7b42c69a..5c37c382 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -20,8 +20,9 @@
 ;; - check what happens if coq-par-coq-arguments gets a bad load path
 ;; - on error, try to put location info into the error message
 ;;
-;; Note that all argument computations inherit coq--pre-v85: when changing
-;; compilers, all compilation jobs must be terminated.
+;; Note that all argument computations inherit `coq-autodetected-version': when
+;; changing compilers, all compilation jobs must be terminated.  This is
+;; consistent with the fact that the _CoqProject file is not reparsed.
 
 (eval-when-compile
   (require 'proof-compat))
@@ -459,7 +460,7 @@ belonging to the circle."
 Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer
 that triggered the compilation, in order to provide correct
 load-path options to coqdep."
-  (nconc (coq-coqdep-prog-args coq-load-path (file-name-directory lib-src-file) coq--pre-v85)
+  (nconc (coq-coqdep-prog-args coq-load-path (file-name-directory lib-src-file) (coq--pre-v85))
          (list lib-src-file)))
 
 (defun coq-par-coqc-arguments (lib-src-file coq-load-path)
@@ -467,7 +468,7 @@ load-path options to coqdep."
 Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer
 that triggered the compilation, in order to provide correct
 load-path options to coqdep."
-  (nconc (coq-coqc-prog-args coq-load-path (file-name-directory lib-src-file) coq--pre-v85)
+  (nconc (coq-coqc-prog-args coq-load-path (file-name-directory lib-src-file) (coq--pre-v85))
          (list lib-src-file)))
 
 (defun coq-par-analyse-coq-dep-exit (status output command)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 4fc56dc5..e00a2793 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -74,7 +74,7 @@ dependencies are absolute too and the simplified treatment of
 break."
   (let ((coqdep-arguments
          ;; FIXME should this use coq-coqdep-prog-args?
-         (nconc (coq-include-options coq-load-path (file-name-directory lib-src-file) coq--pre-v85)
+         (nconc (coq-include-options coq-load-path (file-name-directory lib-src-file) (coq--pre-v85))
 		(list lib-src-file)))
         coqdep-status coqdep-output)
     (if coq-debug-auto-compilation
@@ -113,7 +113,7 @@ Display errors in buffer `coq-compile-response-buffer'."
   (message "Recompile %s" src-file)
   (let ((coqc-arguments
          (nconc
-          (coq-coqc-prog-args coq-load-path (file-name-directory src-file) coq--pre-v85)
+          (coq-coqc-prog-args coq-load-path (file-name-directory src-file) (coq--pre-v85))
 	  (list src-file)))
         coqc-status)
     (coq-init-compile-response-buffer
@@ -122,7 +122,7 @@ Display errors in buffer `coq-compile-response-buffer'."
         (message "call coqc arg list: %s" coqc-arguments))
     (setq coqc-status
           (apply 'call-process
-           coq-compiler nil coq-compile-response-buffer t coqc-arguments))
+                 coq-compiler nil coq-compile-response-buffer t coqc-arguments))
     (if coq-debug-auto-compilation
         (message "compilation %s exited with %s, output |%s|"
                  src-file coqc-status
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 6e51ec16..7664f08a 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -23,16 +23,6 @@
   (defvar coq-prog-args nil)
   (defvar coq-debug nil))
 
-(eval-when (compile)
-  (defvar coq-pre-v85 nil))
-
-(defun get-coq-version ()
-  (let ((c (shell-command-to-string "coqtop -v")))
-    (if (string-match "version \\([^ ]+\\)\\s-" c)
-	(match-string 1 c)
-      c)))
-
-
 (defcustom coq-prog-env nil
   "List of environment settings d to pass to Coq process.
 On Windows you might need something like:
@@ -69,7 +59,7 @@ See also `coq-prog-env' to adjust the environment."
         "/usr/local/lib/coq"
       c)))
 
-(defconst coq-library-directory (get-coq-library-directory)
+(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often
   "The coq library directory, as reported by \"coqtop -where\".")
 
 (defcustom coq-tags (concat coq-library-directory "/theories/TAGS")
@@ -77,12 +67,62 @@ See also `coq-prog-env' to adjust the environment."
   :type 'string
   :group 'coq)
 
-(defcustom coq--pre-v85 nil
-  "Internal setting.
-Tracks whether the current compiler was auto-detected as older than v8.5."
+(defcustom coq-pinned-version nil
+  "Which version of Coq you are using.
+There should be no need to set this value; Proof General can
+adjust to various releases of Coq automatically."
+  :type 'string
+  :group 'coq)
+
+(defvar coq-autodetected-version nil
+  "Version of Coq, as autodetected by `coq-autodetect-version'.")
+
+(defun coq-version (&optional may-recompute)
+  "Return the precomputed version of the current Coq toolchain.
+With MAY-RECOMPUTE, try auto-detecting it if it isn't available."
+  (or coq-pinned-version
+      coq-autodetected-version
+      (when may-recompute
+        (coq-autodetect-version))))
+
+(defun coq-show-version ()
+  "Show the version of Coq currently in use.
+If it doesn't look right, try `coq-autodetect-version'."
+  (interactive)
+  (let ((version (coq-version nil)))
+    (if version
+        (message "Using Coq v%s" coq-autodetected-version)
+      (message "Coq version unknown at this time. Use `coq-autodetect-version' to autodetect."))))
+
+(defun coq-autodetect-version (&optional interactive-p)
+  "Detect and record the version of Coq currently in use.
+Interactively (with INTERACTIVE-P), show that number."
+  (interactive '(t))
+  (setq coq-autodetected-version nil)
+  (let ((version-string (car (process-lines "coqtop" "-v"))))
+    (when (and version-string (string-match "version \\([^ ]+\\)" version-string))
+      (setq coq-autodetected-version (match-string 1 version-string))))
+  (when interactive-p
+    (coq-show-version))
+  coq-autodetected-version)
+
+(defun coq--version< (v1 v2) ;; !!! Check availability in 24.3
+  "Compare Coq versions V1 and V2."
+  (let ((version-regexp-alist  (cons '("^pl$" . 0) version-regexp-alist)))
+    (version< v1 v2)))
+
+(defcustom coq-pre-v85 nil ;; !!! Mark deprecated
+  "Deprecated.
+Use `coq-pinned-version' if you want to bypass the
+version detection that Proof General does automatically."
   :type 'boolean
   :group 'coq)
 
+(defun coq--pre-v85 ()
+  "Return non-nil if the auto-detected version of Coq is < 8.5.
+Returns nil if the version can't be detected."
+  (coq--version< (or (coq-version t) "8.5") "8.5snapshot"))
+
 (defcustom coq-use-makefile nil
   "Whether to look for a Makefile to attempt to guess the command line.
 Set to t if you want this feature, but note that it is deprecated."
@@ -284,7 +324,6 @@ LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
 LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
   ;; coqtop always adds the current directory to the LoadPath, so don't
   ;; include it in the -Q options. ;; !!! Check this comment
-  ;; by the time this function is called, coq-prog-args should be set
   (append (remove "-emacs" (remove "-emacs-U" coq-prog-args))
           (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3
             (coq-coqdep-prog-args coq-load-path current-directory pre-v85))))
@@ -302,7 +341,9 @@ LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'."
   (cons "-emacs" (coq-coqc-prog-args load-path current-directory pre-v85)))
 
 (defun coq-prog-args ()
-  "Wrapper around `coq-coqtop-prog-args' with good defaults."
+  "Recompute `coq-load-path' before calling `coq-coqtop-prog-args'."
+  (coq-load-project-file)
+  (coq-autodetect-version)
   (coq-coqtop-prog-args coq-load-path))
 
 (defcustom coq-use-project-file t
@@ -446,7 +487,7 @@ variable."
 
 (defun coq-load-project-file ()
   "Set `coq-prog-args' and `coq-load-path' according to _CoqProject file.
-Obeys `coq-use-project-file'. Note that if a variable is already
+Obeys `coq-use-project-file'.  Note that if a variable is already
 set by dir/file local variables, this function will not override
 its value.
 See `coq-project-filename' to change the name of the
@@ -461,9 +502,7 @@ feature."
 
 (defun coq-load-project-file-rehack ()
   "Reread file/dir local vars and call `coq-load-project-file'.
-Does nothing if `coq-use-project-file' is nil.
-Warning: 
-"
+Does nothing if `coq-use-project-file' is nil."
   (when coq-use-project-file
     ;; Let us reread dir/file local vars, in case the user mmodified them
     (hack-local-variables)