8.4 compatibility for quick support

8.4 compatibility is done by ignoring all quick settings for
`coq-compile-quick' via a :set function. This does only work if
this variable is only changed via the customization system and
not directly via setq.

1 files changed, 35 insertions, 14 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index e2c43d38..3522a8f0 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -136,6 +136,18 @@ SYMBOL should be 'coq-max-background-compilation-jobs"
   (setq coq--internal-max-jobs new-value)
   (coq-set-max-vio2vo-jobs))
 
+(defun coq-compile-quick-setter (symbol new-value)
+  ":set function for `coq-compile-quick' for pre 8.5 compatibility.
+Ignore any quick setting for Coq versions before 8.5."
+  (cond
+   ((or (eq new-value 'ensure-vo) (eq new-value 'no-quick))
+    t)
+   ((coq--pre-v85)
+    (message "Ignore coq-compile-quick setting %s for Coq before 8.5"
+	     new-value)
+    (setq new-value 'no-quick)))
+  (set symbol new-value))
+
 
 ;;; user options and variables
 
@@ -179,20 +191,28 @@ This option can be set/reset via menu
 
 (defcustom coq-compile-quick 'no-quick
   "Control quick compilation, vio2vo and vio/vo files auto compilation.
-This option controls whether ``-quick'' is used for parallel background
-compilation and whether up-date .vo or .vio files are used or deleted.
-
-Note that ``-quick'' can be noticebly slower when your sources do not
-declare section variables with ``Proof using''. Use the default `no-quick',
-if you have not yet switched to ``Proof using''. Use `quick-no-vio2vo',
-if you want quick recompilation without producing .vo files. Value
-`quick-and-vio2vo' updates missing prerequisites with ``-quick'' and
-starts vio2vo conversion on a subset of the availables cores when the
-quick recompilation finished (see also `coq-compile-vio2vo-percentage').
-Note that all the previously described modes might load .vio files and
-that you therefore might not notice certain universe inconsitencies.
-Finally, use `ensure-vo' for only importing .vo files with complete
-universe checks.
+This option controls whether ``-quick'' is used for parallel
+background compilation and whether up-date .vo or .vio files are
+used or deleted. Please use the customization system to change
+this option to ensure that any ``-quick'' setting is ignored for
+Coq before 8.5.
+
+Note that ``-quick'' can be noticebly slower when your sources do
+not declare section variables with ``Proof using''. Note that
+even if you do declare section variables, ``-quick'' is typically
+slower on small files.
+
+Use the default `no-quick', if you have not yet switched to
+``Proof using''. Use `quick-no-vio2vo', if you want quick
+recompilation without producing .vo files. Value
+`quick-and-vio2vo' updates missing prerequisites with ``-quick''
+and starts vio2vo conversion on a subset of the availables cores
+when the quick recompilation finished (see also
+`coq-compile-vio2vo-percentage'). Note that all the previously
+described modes might load .vio files and that you therefore
+might not notice certain universe inconsitencies. Finally, use
+`ensure-vo' for only importing .vo files with complete universe
+checks.
 
 Detailed description of the 4 modes:
 no-quick         Compile outdated prerequisites without ``-quick'',
@@ -222,6 +242,7 @@ ensure-vo        Delete all .vio files for prerequisites and recompile
     (const :tag "ensure vo compilation, delete vio files" ensure-vo))
   :safe (lambda (v) (member v '(no-quick quick-no-vio2vo
 					 quick-and-vio2vo ensure-vo)))
+  :set 'coq-compile-quick-setter
   :group 'coq-auto-compile)
 
 (defun coq-compile-prefer-quick ()