diff options
author | Hendrik Tews <hendrik@askra.de> | 2016-10-26 23:11:47 +0200 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2016-10-27 09:26:40 +0200 |
commit | f9138553b5fc6fcddc7748c3eb18527773406cc9 (patch) | |
tree | e322ab47e6570cceade9ddb117851a99a94ab7d8 /coq/coq-system.el | |
parent | 8a7eecfa71e850e479822d879e3263c9ce5f2ede (diff) |
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)
Diffstat (limited to 'coq/coq-system.el')
-rw-r--r-- | coq/coq-system.el | 30 |
1 files changed, 27 insertions, 3 deletions
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. |