diff options
-rw-r--r-- | coq/coq-compile-common.el | 49 | ||||
-rw-r--r-- | coq/coq-par-test.el | 11 |
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)) |