From f9138553b5fc6fcddc7748c3eb18527773406cc9 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 26 Oct 2016 23:11:47 +0200 Subject: 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) --- coq/coq-system.el | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'coq/coq-system.el') 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. -- cgit v1.2.3