From f158ae23977cfb40a4a2f7a0db123940f59768f8 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 24 Nov 2016 12:21:06 +0100 Subject: 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. --- coq/coq-compile-common.el | 49 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 35 insertions(+), 14 deletions(-) (limited to 'coq/coq-compile-common.el') 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 () -- cgit v1.2.3