give a more helpful error message if Coq version detection fails

- coq--pre-v85 signals coq-unclassifiable-version for "Invalid
  version" errors
- background compilation converts this into an even more helpful
  message (fixes #70)

2 files changed, 35 insertions, 3 deletions

diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 4ed4c2f8..56539414 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -1367,6 +1367,14 @@ does the error checking/reporting for
       (coq-compile-error
        (coq-par-emergency-cleanup)
        (message "%s %s" (get (car err) 'error-message) (cdr err)))
+      (coq-unclassifiable-version
+       (coq-par-emergency-cleanup)
+       (if (equal (cdr err) "trunkk")
+	   (message
+	    (concat "your Coq version \"trunk\" is too unspecific for "
+		    "Proof General; please customize coq-pinned-version"))
+	 (message "%s \"%s\"; consider customizing coq-pinned-version"
+		  (get (car err) 'error-message) (cdr err))))
       (error
        (message "unexpected error during parallel compilation: %s"
 		err)
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 8df77da0..997e93d2 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -69,14 +69,31 @@ See also `coq-prog-env' to adjust the environment."
 
 (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."
+There should be no need to set this value unless you use the trunk from
+the Coq github repository. For Coq versions with decent version numbers
+Proof General detects the version automatically and adjusts itself. This
+variable should contain nil or a version string."
   :type 'string
   :group 'coq)
 
 (defvar coq-autodetected-version nil
   "Version of Coq, as autodetected by `coq-autodetect-version'.")
 
+;;; error symbols
+
+;; coq-unclassifiable-version
+;;
+;; This error is signaled with one data item -- the bad version string
+
+(put 'coq-unclassifiable-version 'error-conditions
+     '(error coq-unclassifiable-version))
+
+(put 'coq-unclassifiable-version 'error-message
+     "Proof General cannot classify your Coq version")
+
+
+;;; version detection code
+
 (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."
@@ -135,7 +152,14 @@ version detection that Proof General does automatically."
 (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"))
+  (let ((coq-version-to-use (or (coq-version t) "8.5")))
+    (condition-case err
+	(coq--version< coq-version-to-use "8.5snapshot")
+      (error
+       (cond
+	((equal (substring (cadr err) 0 15) "Invalid version")
+	 (signal 'coq-unclassifiable-version  coq-version-to-use))
+	(t (signal (car err) (cdr err))))))))
 
 (defcustom coq-use-makefile nil
   "Whether to look for a Makefile to attempt to guess the command line.