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.

2 files changed, 45 insertions, 15 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 ()
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index 1ce85d0d..c2d3bc9e 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -752,13 +752,22 @@ relative ages.")
 	  ;; a variant is a list of 4 elements
 	  (assert (eq (length variant) 4) nil (concat test-id " 2"))
 	  (let ((files (coq-par-test-flatten-files (car test)))
+		(quick-mode (car variant))
 		(compilation-result (nth 1 variant))
 		(delete-result (nth 2 variant))
 		(req-obj-result (nth 3 variant)))
 	    ;; the delete field, when set, must be a member of the files list
 	    (assert (or (not delete-result)
 			(member delete-result files))
-		    nil (concat test-id " 3"))))
+		    nil (concat test-id " 3"))
+	    ;; 8.4 compatibility check
+	    (when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo))
+		       (not (member 'vio files)))
+	      (assert (not delete-result)
+		      nil (concat test-id " 4"))
+	      (assert (eq compilation-result
+			  (not (eq (car (last (car test))) 'vo)))
+		      nil (concat test-id " 5")))))
 	  (cdr test))))
    coq-par-job-needs-compilation-tests))