diff options
| -rw-r--r-- | CHANGES | 49 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 62 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 53 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 167 | ||||
| -rw-r--r-- | coq/coq-system.el | 16 | ||||
| -rw-r--r-- | coq/coq.el | 148 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 165 | ||||
| -rw-r--r-- | generic/pg-user.el | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 12 | ||||
| -rw-r--r-- | generic/proof-depends.el | 50 |
10 files changed, 555 insertions, 169 deletions
@@ -29,15 +29,22 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac *** new menu Coq -> Auto Compilation for all background compilation options +*** support for 8.11 vos compilation + + See menu Coq -> Auto Compilation -> vos compilation, option + coq-compile-vos and subsection "11.3.3 Quick and inconsistent + compilation" in the Coq reference manual. + *** support for 8.5 quick compilation - See new menu Coq -> Auto Compilation. Select "no quick" as - long as you have not switched to "Proof using" to compile - without -quick. Select "quick no vio2vo" to use -quick - without vio2vo (and guess what "quick and vio2vo" means ;-), - select "ensure vo" to ensure a sound development. See the + See new menu Coq -> Auto Compilation -> Quick compilation. + Select "no quick" as long as you have not switched to "Proof + using" to compile without -quick. Select "quick no vio2vo" to + use -quick without vio2vo (and guess what "quick and vio2vo" + means ;-), select "ensure vo" to ensure a sound development. + Quick compilation is only supported for Coq < 8.11. See the option `coq-compile-quick' or the subsection "11.3.3 Quick - compilation and .vio Files" in the Coq reference manual. + and inconsistent compilation" in the Coq reference manual. *** new option coq-compile-keep-going (in menu Coq -> Auto Compilation) @@ -47,26 +54,16 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac *** Automatic insertion of "Proof using" annotations. - When "Suggest Proof Using" is set in coq, coq suggests "Proof - using" annotations when it detects there is no such annotation (or - a wrong one) in you proof and there should be one (i.r. you are - inside a section). By default PG will ask the user before - inserting the suggested annotation. You can customize this - behaviour: - - (setq coq-accept-proof-using-suggestion 'always) - or - (setq coq-accept-proof-using-suggestion 'never) - or (default) - (setq coq-accept-proof-using-suggestion 'ask) - - This is also settable from Coq menu. - - Limitations: - - do not support nested proofs. - - always use the first suggestion (coq can provide several solutions). - - the proof is not replayed, which is consistent with the fact - that pg do not deal with async proofs. + PG now supports the "Suggest Proof Using" by inserting + (automatically or by contextual menu or by a command) the "Proof + using" annotation suggested by Coq. This suggestion happens at + "Qed" command. By default PG will only highlight the corresponding + "Proof" keyword and let the user actively ask for insertion. You + can customize this behaviour by setting the + coq-accept-proof-using-suggestion to one of these values: 'always, + 'highlight, 'ask, 'never. This is also settable from Coq menu. See + documentation of this variable for an explanation of the different + possible values and some more information. *** Limited extensibility for indentation diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 8db7781e..bd898a9c 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -113,22 +113,6 @@ :selected (eq proof-three-window-mode-policy 'vertical) :help "One column mode"]) ["Refresh Windows Layout" proof-layout-windows t] - ("Automatic Proof using annotations..." - ["ask" - (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) - :style radio - :selected (eq coq-accept-proof-using-suggestion 'ask) - :help "ask user when a new proof using annotation is suggested"] - ["always" - (customize-set-variable 'coq-accept-proof-using-suggestion 'always) - :style radio - :selected (eq coq-accept-proof-using-suggestion 'always) - :help "Always update the proof using annotation when suggested"] - ["never" - (customize-set-variable 'coq-accept-proof-using-suggestion 'never) - :style radio - :selected (eq coq-accept-proof-using-suggestion 'never) - :help "never update the proof using"]) ["Toggle tooltips" proof-output-tooltips-toggle :style toggle :selected proof-output-tooltips @@ -162,7 +146,30 @@ coq-compile-parallel-in-background) :help ,(concat "Continue background compilation after " "the first error as far as possible")] - ("Quick compilation" + ("vos compilation (coq >= 8.11)" + ["unset" + (customize-set-variable 'coq-compile-vos nil) + :style radio + :selected (eq coq-compile-vos nil) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Derive behavior from Quick compilation setting above"] + ["use -vos" + (customize-set-variable 'coq-compile-vos 'vos) + :style radio + :selected (eq coq-compile-vos 'vos) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Speedup with -vos, possibly inconsistent"] + ["ensure vo" + (customize-set-variable 'coq-compile-vos 'ensure-vo) + :style radio + :selected (eq coq-compile-vos 'ensure-vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Ensure only vo's are used for consistency"] + ) + ("Quick compilation (coq < 8.11)" ["no quick" (customize-set-variable 'coq-compile-quick 'no-quick) :style radio @@ -252,6 +259,27 @@ :style radio :selected (eq coq-diffs 'removed) :help "Show diffs: added and removed"]) + ("\"Proof using\" mode..." + ["ask" + (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'ask) + :help "Ask user when a new proof using annotation is suggested"] + ["always" + (customize-set-variable 'coq-accept-proof-using-suggestion 'always) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'always) + :help "Always update the proof using annotation when suggested"] + ["highlight" + (customize-set-variable 'coq-accept-proof-using-suggestion 'highlight) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'highlight) + :help "Highight the proof when an auto insert is suggested (right click to insert))"] + ["Ignore" + (customize-set-variable 'coq-accept-proof-using-suggestion 'ignore) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'ignore) + :help "no highlight (right click insertion still possible)"]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index d29bf1b9..f9a3571e 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -178,7 +178,7 @@ This option can be set/reset via menu (proof-deftoggle coq-compile-before-require) -(defcustom coq-compile-parallel-in-background nil +(defcustom coq-compile-parallel-in-background t "Choose the internal compilation method. When Proof General compiles itself, you have the choice between two implementations. If this setting is nil, then Proof General @@ -203,20 +203,23 @@ This option can be set/reset via menu ;; defpacustom fails to call :eval during inititialization, see trac #456 (coq-switch-compilation-method) -(defcustom coq-compile-quick 'no-quick +(defcustom coq-compile-quick 'quick-and-vio2vo "Control quick compilation, vio2vo and vio/vo files auto compilation. -This option controls whether ``-quick'' is used for parallel +When using coq < 8.11, +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. +Please customize `coq-compile-vos' for coq >= 8.11. + 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 +Use `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'' @@ -280,6 +283,41 @@ This option can be set via menu (eq coq-compile-quick 'quick-no-vio2vo) (eq coq-compile-quick 'quick-and-vio2vo))) +(defcustom coq-compile-vos nil + "Control fast compilation, skipping opaque proofs with ``-vos''. +When using coq >= 8.11, this option controls whether parallel +background compilation is done with ``-vos'', skipping opaque +proofs, thus being considerably faster and inconsistent. + +Set this option to `vos' if you want fast background compilation +and don't care if all proofs are correct. Set this option to +`ensure-vo' if you want all proof and universe constraints +checked carefully. + +For upgrading, if this option is `nil' (i.e., not configured), +then the value of `coq-compile-quick' is considered and vos +compilation is used when `coq-compile-quick' equals +`'quick-no-vio2vo'. + +For coq < 8.11 this option is ignored." + :type + '(radio + (const :tag "unset, derive behavior from `coq-compile-quick'" nil) + (const :tag "use -vos" vos) + (const :tag "ensure vo compilation" ensure-vo)) + :safe (lambda (v) (member v '(nil vos ensure-vo))) + :group 'coq-auto-compile) + +(defun coq-compile-prefer-vos () + "Decide whether ``-vos'' should be used. +This function implements the upgrade path for fast compilation, +by checking the value of `coq-compile-quick' if `coq-compile-vos' +is nil." + (or + (eq coq-compile-vos 'vos) + (and (not coq-compile-vos) + (eq coq-compile-quick 'quick-no-vio2vo)))) + (defcustom coq-compile-keep-going t "Continue compilation after the first error as far as possible. Similar to ``make -k'', with this option enabled, the background @@ -556,9 +594,14 @@ Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"." (defun coq-library-vio-of-vo-file (vo-obj-file) "Return .vio file name for VO-OBJ-FILE. -Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." +Changes the suffix from .vo to .vio. VO-OBJ-FILE must have a .vo suffix." (concat (coq-library-src-of-vo-file vo-obj-file) "io")) +(defun coq-library-vos-of-vo-file (vo-obj-file) + "Return .vok file name for VO-OBJ-FILE. +Changes the suffix from .vo to .vok. VO-OBJ-FILE must have a .vo suffix." + (concat vo-obj-file "s")) + ;;; ancestor unlocking ;;; (locking is different for sequential and parallel compilation) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index c700533d..9c05dbde 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -24,8 +24,6 @@ ;;; TODO ;; ;; - fix -I current-dir argument for coqc invocations -;; - add option coq-par-keep-compilation-going -;; - check what happens if coq-par-coq-arguments gets a bad load path ;; - on error, try to put location info into the error message ;; ;; Note that all argument computations inherit `coq-autodetected-version': when @@ -45,7 +43,7 @@ ;; This file implements parallel background compilation. It makes sure ;; that only a certain number (`coq-max-background-compilation-jobs') -;; of coqdep anc coqc processes are running in the background. +;; of coqdep and coqc processes are running in the background. ;; ;; In this file, compilation jobs are uninterned lisp symbols that ;; store all important information in their property list. New @@ -66,7 +64,8 @@ ;; 1- where to put the Require command and the items that follow it ;; 2- make sure ancestors are properly locked ;; 3- error reporting -;; 4- using -quick and the handling of .vo/.vio prerequisites +;; 4- using -quick and the handling of .vo/.vio prerequisites for Coq < 8.11 +;; 5- using -vos for Coq >= 8.11 ;; ;; For 1- where to put the Require command and the items that follow it: ;; @@ -146,8 +145,15 @@ ;; the last top-level job is delayed until proof-action-list is empty. ;; Then the whole queue is deleted. ;; -;; For 4- using -quick and the handling of .vo/.vio prerequisites +;; For 4- using -quick and the handling of .vo/.vio prerequisites for Coq < 8.11 ;; +;; There are now two ways available to speed up compilation, +;; -quick/-vio and -vos. For Coq >= 8.5 and < 8.11 -quick/-vio is +;; available and coq-compile-quick is consulted in order to determine +;; whether to use it. For Coq >= 8.11 -vos is available and +;; coq-compile-vos is consulted. The following paragraph descripes the +;; complications with -quick/-vio. + ;; Coq accepts both .vo and .vio files for importing modules ;; regardless of it is running with -quick or not. However, it is ;; unclear which file is loaded when both, .vo and .vio, of a @@ -164,6 +170,26 @@ ;; .vo file and if already present .vo or .vio files must be deleted. ;; Only at that point the relevant property 'required-obj-file is set. ;; +;; For 5- using -vos for Coq >= 8.11 +;; +;; When Coq >= 8.11 is detected, -vos is used and coq-compile-vos is +;; consulted in order to find out whether to compile to .vos or to .vo +;; files. For people switching PG or switching to Coq 8.11, there is a +;; backward compatibility path: When coq-compile-vos is nil, the +;; decision is derived from coq-compile-quick. +;; +;; The logic here to decide whether compilation is needed or not, +;; assumes coq is used consistently without randomly deleting files. +;; Because coqc always produces an empty .vos file when compiling to +;; .vo, it can never happen, that a .vo file is present without .vos +;; file or that a .vo file is more recent then the corresponding .vos +;; file. This simplifies the logic for deciding about recompilation +;; quite a bit. +;; +;; For Coq >= 8.11, vio to vo compilation is disabled for obvious +;; reasons and in this version of Proof General, there is no similar +;; feature. +;; ;; ;; Properties of compilation jobs ;; @@ -180,8 +206,10 @@ ;; 'obj-mod-time - modification time of 'required-obj-file, stored ;; here, to avoid double stat calls; ;; contains 'obj-does-not-exist in case that file is absent -;; 'use-quick - t if `coq-par-job-needs-compilation' decided to use -;; -quick +;; 'use-quick - 'vio if `coq-par-job-needs-compilation' decided to use +;; -quick for Coq older than 8.11; 'vos if it decided to +;; to use -vos for Coq 8.11 or newer, nil if it decided +;; to use .vo compilation or no compilation is necessary. ;; 'type - the type of the job, either 'clone or 'file ;; for real compilation jobs ;; 'state - the state of the job, see below @@ -276,6 +304,29 @@ ;; the process is killed ;; ;; +;; Over its live time, a compilation job might get passed through the +;; following functions. Some of them might be skipped or executed more +;; then once. +;; +;; | function | state | comment | +;; |----------------------------------+------------------+--------------------------------------| +;; | coq-par-create-library-job | 'enqueued-coqdep | job creation | +;; | coq-par-start-coqdep | | | +;; | coq-par-process-coqdep-result | 'waiting-dep | create dependee/child jobs | +;; | coq-par-decrease-coqc-dependency | | dependee/child finished coqc | +;; | coq-par-compile-job-maybe | 'enqueued-coqc | | +;; | -- start coqc | | | +;; | coq-par-coqc-continuation | | | +;; | coq-par-kickoff-coqc-dependants | 'waiting-queue | | +;; | coq-par-kickoff-queue-maybe | ready | | +;; | coq-par-retire-top-level-job | | | +;; | coq-par-require-processed | | in dummy action in proof-action-list | +;; | coq-par-run-vio2vo-queue | | called via timer | +;; | coq-par-start-vio2vo | | | +;; | coq-par-vio2vo-continuation | | | +;; +;; +;; The following is maybe outdated. ;; To print the states of the compilation jobs for debugging, eval ;; ;; (let ((clones)) @@ -303,6 +354,7 @@ ;; (get v 'queue-dependant))) ;; clones)) + ;;; Variables (defvar coq--current-background-jobs 0 @@ -844,6 +896,7 @@ This function starts COMMAND with arguments ARGUMENTS for compilation job JOB, making sure that CONTINUATION runs when the process finishes successfully. FILE-RM, if non-nil, denotes a file to be deleted when the process is killed." + ;; (message "CPSP %s %s %s %s %s" command arguments continuation job file-rm) (let ((process-connection-type nil) ; use pipes (process-name (format "pro-%s" coq--par-next-id)) process) @@ -1020,15 +1073,15 @@ somewhere after the last require command." (message "%s -> %s: add queue dependency" (get dependee 'name) (get dependant 'name)))) -(defun coq-par-job-needs-compilation (job) +(defun coq-par-job-needs-compilation-quick (job) "Determine whether JOB needs to get compiled and do some side effects. This function contains most of the logic nesseary to support -quick compilation according to `coq-compile-quick'. Taking +quick compilation according to `coq-compile-quick' for coq < 8.11. Taking `coq-compile-quick' into account, it determines if a compilation is necessary. The property 'required-obj-file is set either to the file that we need to produce or to the up-to-date object -file. If compilation is needed, property 'use-quick is set when --quick will be used. If no compilation is needed, property +file. If compilation is needed, property 'use-quick is set to `vio' when +-quick/-vio will be used. If no compilation is needed, property 'obj-mod-time remembers the time stamp of 'required-obj-file. Indepent of whether compilation is required, .vo or .vio files that are in the way are deleted. Note that the coq documentation @@ -1087,7 +1140,7 @@ therefore delete a file if it might be in the way. Sets the (if (coq-compile-prefer-quick) (progn (put job 'required-obj-file vio-file) - (put job 'use-quick t) + (put job 'use-quick 'vio) (when vo-obj-time (setq file-to-delete vo-file)) (when (eq coq-compile-quick 'quick-and-vio2vo) @@ -1188,6 +1241,79 @@ therefore delete a file if it might be in the way. Sets the (signal 'coq-compile-error-rm err)))) result)) +(defun coq-par-job-needs-compilation-vos (job) + "Determine whether JOB needs to get compiled. +This function decides whether JOB needs to get compiled for coq +>= 8.11 and whether a .vo or a .vos should be produced. For the +latter, `coq-compile-vos' is consulted and, if that is `nil', +coq-compile-quick, see `coq-compile-prefer-vos'. This function +assumes that coq is used consistently and that a .vo file cannot +be present without a .vos file that has the same time stamp of +has been created more recently. As result, this function sets the +property 'use-quick to `vos' if JOB should be compiled with -vos. +If no compilation is needed, 'obj-mod-time to the time stamp of +the .vos or .vo file, depending on `coq-compile-prefer-vos'." + (let* ((vo-file (get job 'vo-file)) + (vos-file (coq-library-vos-of-vo-file vo-file)) + (dep-time (get job 'youngest-coqc-dependency)) + (src-time (nth 5 (file-attributes (get job 'src-file)))) + (vos-obj-time (nth 5 (file-attributes vos-file))) + result) + (when coq--debug-auto-compilation + (message "%s: compare mod times: vos mod %s, src mod %s, youngest dep %s" + (get job 'name) + (if vos-obj-time (current-time-string vos-obj-time) "-") + (if src-time (current-time-string src-time) "-") + (if (eq dep-time 'just-compiled) "just compiled" + (current-time-string dep-time)))) + (if (or (eq dep-time 'just-compiled) ; a dep has been just compiled + (not vos-obj-time) ; neither vos nor vo present + ;; src younger than vos? + (time-less-or-equal vos-obj-time src-time) + ;; dep younger than vos? + (time-less-or-equal vos-obj-time dep-time)) + ;; compilation needed + (if (coq-compile-prefer-vos) + (progn + (put job 'required-obj-file vos-file) + (put job 'use-quick 'vos) + (setq result t)) + (put job 'required-obj-file vo-file) + (setq result t)) + ;; maybe need to compile if vo is required + (if (coq-compile-prefer-vos) + ;; vo not required and vos is fine - no compilation + (put job 'obj-mod-time vos-obj-time) + ;; vo required, may need to compile + (let ((vo-obj-time (nth 5 (file-attributes vo-file)))) + (when coq--debug-auto-compilation + (message "%s: ensure-vo: vo mod %s" + (get job 'name) + (if vo-obj-time (current-time-string vo-obj-time) "-"))) + (if (or (not vo-obj-time) ; vo not present + ;; src younger than vo? + (time-less-or-equal vo-obj-time src-time) + ;; dep younger than vo? + (time-less-or-equal vo-obj-time dep-time)) + ;; compilation needed + (progn + (put job 'required-obj-file vo-file) + (setq result t)) + ;; vo is fine - no compilation + (put job 'obj-mod-time vo-obj-time))))) + result)) + +(defun coq-par-job-needs-compilation (job) + "Determine if JOB nees to get compiled and possibly do some side effects. +This function calls `coq-par-job-needs-compilation-vos for coq >= +8.11 and `coq-par-job-needs-compilation-quick' otherwise. Returns +t if a compilation is required and sets the 'use-quick property +depending on wheter -quick/-vio or -vos should be used. Property +'obj-mod-time is set when no compilation is needed." + (if (coq--post-v811) + (coq-par-job-needs-compilation-vos job) + (coq-par-job-needs-compilation-quick job))) + (defun coq-par-retire-top-level-job (job) "Register ancestors and start queue items. This function performs the essential tasks for top-level jobs @@ -1215,7 +1341,8 @@ function must not be called for failed jobs." (push (get anc-job 'src-file) (span-property span 'coq-locked-ancestors))))) (when items - (when (and (eq coq-compile-quick 'quick-and-vio2vo) + (when (and (not (coq--post-v811)) + (eq coq-compile-quick 'quick-and-vio2vo) (eq coq--last-compilation-job job)) (let ((vio2vo-counter (setq coq--compile-vio2vo-start-id @@ -1308,7 +1435,8 @@ case, the following actions are taken: (with-current-buffer (or proof-script-buffer (current-buffer)) (proof-script-clear-queue-spans-on-error nil)) (proof-release-lock) - (when (eq coq-compile-quick 'quick-and-vio2vo) + (when (and (coq--post-v811) + (eq coq-compile-quick 'quick-and-vio2vo)) (cl-assert (not coq--compile-vio2vo-delay-timer) nil "vio2vo timer set before last compilation job") (setq coq--compile-vio2vo-delay-timer @@ -1500,12 +1628,17 @@ coqdep or coqc are started for it." (coq-par-start-coqdep job)) ((eq job-state 'enqueued-coqc) (message "Recompile %s%s" - (if (get job 'use-quick) "-quick " "") + (cond + ((eq (get job 'use-quick) 'vos) "-vos ") + ((eq (get job 'use-quick) 'vio) "-quick ") + (t "")) (get job 'src-file)) (let ((arguments (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path)))) - (when (get job 'use-quick) - (push "-quick" arguments)) + (cond + ((eq (get job 'use-quick) 'vos) (push "-vos" arguments)) + ((eq (get job 'use-quick) 'vio) (push "-quick" arguments)) + (t t)) (coq-par-start-process coq-compiler arguments diff --git a/coq/coq-system.el b/coq/coq-system.el index e2a3431e..637e0a27 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -59,8 +59,8 @@ On Windows you might need something like: :group 'coq) (defcustom coq-pinned-version nil - "Which version of Coq you are using. -There should be no need to set this value unless you use the trunk from + "Manual coq version override (rarely needed). +There should be no need to set this value unless you use old trunk versions 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." @@ -197,6 +197,18 @@ Return nil if the version cannot be detected." (signal 'coq-unclassifiable-version coq-version-to-use)) (t (signal (car err) (cdr err)))))))) +(defun coq--post-v811 () + "Return t if the auto-detected version of Coq is >= 8.11. +Return nil if the version cannot be detected." + (let ((coq-version-to-use (or (coq-version t) "8.10"))) + (condition-case err + (not (coq--version< coq-version-to-use "8.11")) + (error + (cond + ((equal (substring (cadr err) 0 15) "Invalid version") + (signal 'coq-unclassifiable-version coq-version-to-use)) + (t (signal (car err) (cdr err)))))))) + (defun coq--supports-topfile () "Return t if \"-topfile\" appears in coqtop options" (string-match "-topfile" coq-autodetected-help) @@ -109,7 +109,9 @@ Namely, goals that do not fit in the goals window." ;TODO: remove Set Undo xx. It is obsolete since coq-8.5 at least. ;;`(,(format "Set Undo %s . " coq-default-undo-limit) "Set Printing Width 75.") (defconst coq-shell-init-cmd - (append `(,(format "Add Search Blacklist %s. " coq-search-blacklist-string)) coq-user-init-cmd) + (append `(,(format "Add Search Blacklist %s. " coq-search-blacklist-string)) + '("Set Suggest Proof Using. ") + coq-user-init-cmd) "Command to initialize the Coq Proof Assistant.") @@ -1972,6 +1974,8 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-no-fully-processed-buffer t + proof-dependency-menu-system-specific coq-dependency-menu-system-specific + proof-dependencies-system-specific coq-dependencies-system-specific ;; Coq has no global settings? ;; (proof-assistant-settings-cmd) @@ -2564,52 +2568,124 @@ Warning: this makes the error messages (and location) wrong.") ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; (setq coq-shell-theorem-dependency-list-regexp - "<infomsg>\\(?: \\|\n\\)The proof of \\([^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\([^.]*\\)\\.") - -(defcustom accept-proof-using-suggestion 'ask - "Wether proofgeneral should automatically update proof using when -recieving suggestions from coq at Qed time." + "<infomsg>\n?The proof of \\([^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\([^.]*\\)\\.") + +(defcustom coq-accept-proof-using-suggestion 'highlight + "Wether and how proofgeneral should insert \"Proof using\" suggestions. +Suggestions are emitted by Coq at Qed time. The possible values +of this variable are: + +- 'always: always insert the suggested annotation + +- 'highlight (default value): highlight the Proof command and + have a contextual menu for insertion (or M-x + coq-insert-suggested-dependency when point is on the proof + considered) + +- 'ask: asks the user each time. If yes then do as 'always, else + do as 'highlight + +- 'never: ignore completely the suggestions. + +Remarks and limitations: +- do not support nested proofs. +- always use the *first* annotation suggested by coq. +- the proof is not replayed, which is consistent with the fact + that pg currently do not deal with async proofs. +- if there is already a \"Proof using\" annotation, then either it + is correct and nothing happens, or it is incorrect and coq + generates an error. PG won't try to replace the erroneous + annotation in this case, but you can always go back, remove it + by hand, and let pg insert the good one. +- instead of the menu you can do M-x coq-insert-suggested-dependency + when point is on the proof considered. +" :type '(choice (const :tag "Ask user" ask) - (const :tag "always accept" always) - (const :tag "never accept" never)) + (const :tag "Always accept" always) + (const :tag "Higihlight" never) + (const :tag "Ignore completely" ignore)) :group 'coq) -(defun coq-extract-proof-using-from-suggestion (span) - (let ((sp (span-property-safe span 'dependencies))) - sp)) - -(defun coq-insert-proof-using-suggestion (span suggested) +;; the additional menu for "proof using". highlights the "Proof." command, and +;; have a entry to insert the annotation and remove the highlight. +(defvar coq-dependency-menu-system-specific + (lambda (span) + (let* ((deps (span-property-safe span 'dependencies)) + (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) + (specialspan (and specialspans (not (cdr specialspans)) (car specialspans))) + (name (concat " insert \"proof using " (mapconcat 'identity deps " ") "\"")) + (fn `(lambda (sp) + (coq-insert-proof-using-suggestion sp t) + (span-delete ,specialspan)))) + (list "-------------" (vector name `(,fn ,span) t)))) + "Coq specific additional menu entry for \"Proof using\". +annotation. See `proof-dependency-menu-system-specific'." ) + +(defconst coq-proof-using-regexp "\\_<Proof\\(?:\\s-+using\\>\\)?\\([^.]*\\)\\." + "regexp matching Coq \"Proof( using xxx)?.\" annotation. +There should be one subexp numbered 1 matching xxx if present.") + +(defun coq-mark-span-dependencies (span suggested) + (goto-char (span-start span)) + (let* ((endpos (re-search-forward coq-proof-using-regexp)) + (proof-pos (match-beginning 0)) + (newspan (span-make proof-pos endpos))) + (span-set-property newspan 'face 'proof-warning-face) + (span-set-property newspan 'help-echo "Right click to insert \"proof using\"") + (span-set-property newspan 'proofusing t))) + +(defun coq-insert-proof-using (proof-pos previous-content string-suggested) + (goto-char (+ 5 proof-pos)) ; "Proof" has length 6 + (let ((spl proof-locked-span)) + (span-read-write spl) ; temporarily make the locked span writable + (when previous-content (delete-char (length previous-content))) + (insert (concat " using " string-suggested)) + (proof-span-read-only spl))) + +(defun coq-insert-suggested-dependency () + (interactive) + (let* ((span (span-at (point) 'type)) + (deps (span-property-safe span 'dependencies)) + (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) + (specialspan (and specialspans (not (cdr specialspans)) (car specialspans)))) + (coq-insert-proof-using-suggestion span t) + (span-delete specialspan))) + +;; TODO: have 'ignoe option to completely ignore (not highlight) +;; and have 'never renamed into 'highlight +(defun coq-insert-proof-using-suggestion (span &optional force) "Add the proof using annotation, respecting `coq-accept-proof-using-suggestion'. Insert \" using xxx\" After the \"Proof\" of SPAN, where xxx is built from the list of strings in SUGGESTED." (with-current-buffer proof-script-buffer (save-excursion (goto-char (span-start span)) - (let* ((pos-unproc (point)) - (endpos (save-excursion - (search-forward-regexp "\\<Proof\\(?:\\s-+using\\)?\\>\\([^.]*\\)\\."))) - (proof-pos (and endpos (match-beginning 0))) - (previous-content (and endpos (split-string (match-string 1)))) - (string-suggested (mapconcat 'identity suggested " ")) - (same (and endpos (not (cl-set-exclusive-or previous-content suggested :test 'string-equal))))) - (when (and endpos (not same) - (or (equal coq-accept-proof-using-suggestion 'always) + (let* ((endpos (re-search-forward coq-proof-using-regexp))) + (when endpos + (let* ((suggested (span-property span 'dependencies)) + (proof-pos (match-beginning 0)) + (previous-content (split-string (match-string 1))) + (string-suggested (mapconcat 'identity suggested " ")) + (same (and previous-content + (not (cl-set-exclusive-or previous-content suggested + :test 'string-equal)))) + (usersayyes + (and (not same) (not force) + (equal coq-accept-proof-using-suggestion 'ask) (y-or-n-p (concat "Update proof using annotation (" - string-suggested ")")))) - (goto-char (+ 5 proof-pos)) ; "Proof" has length 6 - ;(if (stored proof-strict-read-only) ) - (let ((spl proof-locked-span)) - ;; temporarily make the locked span writable - (span-read-write spl) - (delete-char (length previous-content)) - (insert (concat " using " string-suggested)) - ;; go back to `proof-strict-read-only' says - (proof-span-read-only spl))))))) - -(defun proof-dependencies-system-specific (name span) - (let ((suggested (coq-extract-proof-using-from-suggestion span))) - (coq-insert-proof-using-suggestion span suggested))) + string-suggested ")"))))) + (unless same + (if (or force (equal coq-accept-proof-using-suggestion 'always) usersayyes) + (coq-insert-proof-using proof-pos previous-content string-suggested) + (when (member coq-accept-proof-using-suggestion '(highlight ask)) + (coq-mark-span-dependencies span suggested) + (message "\"Proof using\" not set. M-x coq-insert-suggested-dependency or right click to add it. See also `coq-accept-proof-using-suggestion'.")))))))))) + +(defvar coq-dependencies-system-specific + (lambda (span) (coq-insert-proof-using-suggestion span)) + "Coq specific dependency mechanism. +Used for automatic insertion of \"Proof using\" annotations.") ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index c2cb3be5..24d4d7e8 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4462,6 +4462,39 @@ path (including the -R lib options) (see @samp{@code{coq-load-path}}). You can also use the .dir-locals.el as above to configure this setting on a per project basis. +@node Proof using annotations +@section Proof using annotations + +In order to process files asynchronously and pre-compile files (.vos and +.vok files), it is advised (inside sections) to list the section +variables (and hypothesis) on which each lemma depends on. This must be +done at the beginning of a proof with this syntax: + +@verbatim +Lemma foo: ... . +Proof using x y H1 H2. +@end verbatim + +If the annotation is missing, then at Qed time (i.e. later in the +script) coq complains with a warning and a suggestion of a correct +annotation that should be added. ProofGeneral intercepts this suggestion +and stores relevant information. Then depending on user preference it +can either +@itemize @bullet +@item insert immediately the ``using...'' annotation after ``Proof'', +without replaying the proof. +@item highlight the place where the annotation should be inserted and +allow the user to perform the insertion later either via right click +menu on the proof or by @code{M-x coq-insert-suggested-dependency} (it +won't replay the proof) +@item ask the user each time which of the two solutions above he wants +@item ignore completely the suggestion. +@end itemize + +This can be configured either via Coq menu or by setting variable +@code{coq-accept-proof-using-suggestion} to one of the following values: +@code{'always}, @code{'highlight}, @code{'ask} or @code{'never}. + @node Multiple File Support @section Multiple File Support @@ -4482,10 +4515,10 @@ buffer depends. This is controlled by the user option @ref{Locking Ancestors}. @item (Re-)Compilation Before a @code{Require} command is processed it may be necessary -to save and compile some buffers. Because this feature -conflicts with existing customization habits, it is switched off -by default. When it is properly configured, one can freely switch -between different buffers. Proof General will compile the +to save some buffers and compile some files. When automatic +(re-)compilation is enabled (it's off by default), one can freely +work in different buffers within one Proof General session. +Proof General will compile the necessary files whenever a @code{Require} command is processed. The compilation feature does currently not support ML modules. @@ -4499,12 +4532,14 @@ feature. With parallel compilation, coqdep and coqc are launched in the background and Proof General stays responsive during compilation. Up to `coq-max-background-compilation-jobs' coqdep and coqc -processes may run in parallel. Coq 8.5 quick compilation is -supported with various modes, @ref{Quick compilation and .vio Files}. +processes may run in parallel. Compiled interfaces (@code{-vos} +for Coq 8.11 or newer) and quick compilation +(@code{-quick}/@code{-vio} for Coq 8.5 or newer) is +supported with various modes, @ref{Quick and inconsistent compilation}. @item Synchronous single threaded compilation (obsolete) With synchronous compilation, coqdep and coqc are called synchronously for each Require command. Proof General is locked -until the compilation finishes. Coq 8.5 quick compilation is not +until the compilation finishes. Neither quick nor vos compilation is supported with synchronously compilation. @end table @@ -4515,10 +4550,8 @@ these points: @item Set the option @code{coq-compile-before-require} (menu @code{Coq -> Auto Compilation -> Compile Before Require}) to enable -compilation before processing @code{Require} commands and set -@code{coq-compile-parallel-in-background} (menu @code{Coq --> Auto Compilation -> Parallel background compilation}) for -parallel asynchronous compilation (recommended). +compilation before processing @code{Require} commands. By +default, this enables parallel asynchronous compilation. @item Nonstandard load path elements @emph{must} be configured via a Coq project file (this is the recommended option), @@ -4545,7 +4578,7 @@ single threaded compilation, simply hit @code{C-g}. @menu * Automatic Compilation in Detail:: * Locking Ancestors:: -* Quick compilation and .vio Files:: +* Quick and inconsistent compilation:: * Customizing Coq Multiple File Support:: * Current Limitations:: @end menu @@ -4561,9 +4594,11 @@ the queue region, @ref{Locked queue and editing regions}). If Proof General finds a @code{Require} command, it checks the dependencies and (re-)compiles files as necessary. The Require command and the following text is only sent to Coq after the -compilation finished. +compilation has finished. -@code{Declare ML Module} commands are currently not recognized. +@code{Declare ML Module} commands are currently not recognized +and dependencies on ML Modules reported by @code{coqdep} are +ignored. Proof General uses @code{coqdep} in order to translate the qualified identifiers in @code{Require} commands to coq library @@ -4581,10 +4616,14 @@ Sometimes the compilation commands do not produce error messages with location information, then @code{C-x `} does only work in a limited way. -For Coq version 8.5 or newer, the option @code{coq-compile-quick} -controls how @code{-quick} and @code{.vio} files are used, -@ref{Quick compilation and .vio Files}. This can also be -configured in the menu @code{Coq -> Auto Compilation}. +Proof General supports both vos and quick/vio +compilation to speed up compilation of required modules at the +price of consistency. Because quick/vio compilation does not seem +to have a benefit with vos compilation present, the former is +only supported for Coq before 8.11. Both can be configured via +the settings @code{coq-compile-vos} and @code{coq-compile-quick} +and via menu entries in @code{Coq -> Auto Compilation}, +@ref{Quick and inconsistent compilation}. Similar to @code{make -k}, background compilation can be configured to continue as far as possible after the first error, @@ -4615,11 +4654,12 @@ locked until compilation finishes. Use @code{C-g} to interrupt compilation. This method supports compilation via an external command (such as @code{make}), see option @code{coq-compile-command} in @ref{Customizing Coq Multiple File -Support} below. Synchronous compilation does not support the -quick compilation of Coq 8.5. +Support} below. Synchronous compilation does neither support +quick/vio nor vos compilation. @item Parallel asynchronous compilation -This is the newer and default version added in Proof General version 4.3. It +This is the newer, recommended +and default version added in Proof General version 4.3. It runs up to @code{coq-max-background-compilation-jobs} coqdep and coqc jobs in parallel in asynchronous subprocesses (or uses all your CPU cores if @code{coq-max-background-compilation-jobs} @@ -4639,15 +4679,11 @@ before the first Require, then you may see Proof General and Coq running in addition to `coq-max-background-compilation-jobs' compilation jobs. -Depending on the setting of @code{coq-compile-quick} (which can -also be set via menu @code{Coq -> Auto Compilation}) Proof -General produces @code{.vio} or @code{.vo} files and deletes -outdated @code{.vio} or @code{.vo} files to ensure Coq does not -load outdated files. When @code{quick-and-vio2vo} is selected a -vio2vo compilation starts when the @code{Require} command had -been processed, @ref{Quick compilation and .vio Files}. +Parallel asynchronous compilation supports both vos and quick/vio +compilation, but exclusively, depending on the Coq version, +@ref{Quick and inconsistent compilation}. -Actually, even with this method, not everything runs +Actually, even with parallel asynchronous compilation, not everything runs asynchronously. To translate module identifiers from the Coq sources into file names, Proof General runs coqdep on an automatically generated, one-line file. These coqdep jobs run @@ -4673,7 +4709,7 @@ forced to completely retract the current scripting buffer. You can simplify this by setting @code{proof-strict-read-only} to @code{'retract} (menu @code{Proof-General -> Quick Options -> Read Only -> Undo On Edit}). Then typing in some ancestor will -immediately retract you current scripting buffer and unlock that +immediately retract your current scripting buffer and unlock that ancestor. You have two choices, if you don't like ancestor locking in its @@ -4696,19 +4732,54 @@ benefit, as Require commands are usually on the top of each file.] -@node Quick compilation and .vio Files -@subsection Quick compilation and .vio Files +@node Quick and inconsistent compilation +@subsection Quick and inconsistent compilation + +Coq now supports two different modes for speeding up compilation +at the price of consistency. Since Coq 8.11, @code{-vos} compiles +interfaces into @code{.vos} files and since Coq 8.5 +@code{-quick}/@code{-vio} produces @code{.vio} files. Proof +General supports both modes with parallel asynchronous +compilation, but exclusively, depending on the detected Coq +version. For Coq 8.11 or newer only @code{-vos} can be used. +There are a number of different compilation options supported, +see below. -Proof General supports quick compilation only with the parallel -asynchronous compilation. There are 4 modes that can be +For Coq 8.11 or newer (decided by the automatic Coq version +detection of Proof General or by the setting +@code{coq-pinned-version}) required modules are either compiled +to @code{.vo} or @code{.vos} files, depending on the setting +@code{coq-compile-vos}, which can also be set on menu @code{Coq +-> Auto Compilation -> vos compilation}. There are three choices: + +@table @asis +@item @code{use-vos} +Compile with @code{-vos}. Noticeably faster, but proofs are +skipped during compilation and some universe constraints might be +missing. +@item @code{ensure-vo} +Compile without @code{-vos} to @code{.vo} files, checking all +proofs and universe constraints. +@item unset (@code{nil}) +Compile with @code{-vos} if @code{coq-compile-quick} (see below) +equals @code{quick-no-vio2vo}. Otherwise compile without +@code{-vos} to @code{.vo}. This value provides an upgrade path +for users that configured @code{coq-compile-quick} in the past. +@end table + +For Coq version 8.5 until before 8.11, Proof General supports +quick or vio compilation with parallel asynchronous compilation. +There are 4 modes that can be configured with @code{coq-compile-quick} or by selecting one of the radio buttons in the @code{Coq -> Auto Compilation -> Quick -compilation} menu. +compilation} menu. For Coq before 8.11 @code{coq-compile-vos} is +ignored. -Use the default @code{no-quick}, if you have not yet switched to +Value @code{no-quick} was provided for the transition, for those +that have not switched there development to @code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick recompilation without producing .vo files. Option -@code{quick-and-vio2vo} recompiles with @code{-quick} as +@code{quick-and-vio2vo} recompiles with @code{-quick}/@code{-vio} as @code{quick-no-vio2vo} does, but schedules a vio2vo compilation for missing @code{.vo} files after a certain delay. Finally, use @code{ensure-vo} for only importing @code{.vo} files with @@ -4716,10 +4787,11 @@ complete universe checks. Note that with all of @code{no-quick}, @code{quick-no-vio2vo} and @code{quick-and-vio2vo} your development might be unsound because +proofs might have been skipped and universe constraints are not fully present in @code{.vio} files. There are a few peculiarities of quick compilation in Coq 8.5 -that one should be aware of. +and possibly also in other versions. @itemize @item @@ -4732,7 +4804,7 @@ comparatively big size of the @code{.vio} files. You can speed up quick compilation noticeably by running on a RAM disk. @item If both, the @code{.vo} and the @code{.vio} files are present, -Coq load the more recent one, regardless of whether +Coq loads the more recent one, regardless of whether @code{-quick}, and emits a warning when the @code{.vio} is more recent than the @code{.vo}. @item @@ -4753,7 +4825,8 @@ To ensure soundness, all library dependencies must be compiled as @code{.vo} files and loaded into one Coq instance. @end itemize -Detailed description of the 4 modes: +Detailed description of the 4 possible settings of +@code{coq-compile-quick}: @table @code @item no-quick @@ -4863,8 +4936,9 @@ This option can be set/reset via menu @end defvar -The option @code{coq-compile-quick} is described in detail above, -@ref{Quick compilation and .vio Files} +The options @code{coq-compile-vos} and @code{coq-compile-quick} +are described in detail above, @ref{Quick and inconsistent +compilation}. @c TEXI DOCSTRING MAGIC: coq-compile-keep-going @@ -5047,7 +5121,12 @@ or not. @itemize @item -No support @code{Declare ML Module} commands. +No support for @code{Declare ML Module} commands and files +depending on an ML module. +@item +Comments inside require commands should be avoided, see Proof +General issue #352. The regular expression to extract module +names does not skip over comments. @item When a compiled library has the same time stamp as the source file, it is considered outdated. Some old file systems (for diff --git a/generic/pg-user.el b/generic/pg-user.el index d2259ef8..f10f02c1 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -770,7 +770,7 @@ If NUM is negative, move upwards. Return new span." (list (pg-span-name span)) (list (vector "Show/hide" - (if idiom (list 'pg-toggle-element-visibility (quote idiom) name)) + (if idiom (list 'pg-toggle-element-visibility `(quote ,idiom) name)) (not (not idiom)))) (list (vector "Copy" (list 'pg-copy-span-contents span) t)) diff --git a/generic/proof-config.el b/generic/proof-config.el index 41c5e9d7..c10c0ee0 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1760,7 +1760,17 @@ This hook is used within Proof General to refresh the toolbar." ;;;;;; (defcustom proof-dependencies-system-specific nil - "doc TODO" + "Set this variable to handle system specific dependency output. +This must be a function with 1 parameter: the goalsave span of +the theorem being saved." + :type '(repeat function) + :group 'proof-shell) + +(defcustom proof-dependency-menu-system-specific nil + "Hook for system specific menu items for dependency menu. +This must be a function taking one argument: the span one which +the secific menu must be added. It must return a lit with the +same type as `proof-dependency-in-span-context-menu' returns." :type '(repeat function) :group 'proof-shell) ;;;;; diff --git a/generic/proof-depends.el b/generic/proof-depends.el index c3de97f7..6651e277 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -121,7 +121,7 @@ Called from `proof-done-advancing' when a save is processed and (span-set-property gspan 'dependencies-within-file depspans) (setq proof-last-theorem-dependencies nil) - (funcall 'proof-dependencies-system-specific name gspan))) + (funcall proof-dependencies-system-specific gspan))) @@ -136,27 +136,35 @@ Called from `proof-done-advancing' when a save is processed and ;;;###autoload (defun proof-dependency-in-span-context-menu (span) - "Make some menu entries showing proof dependencies of SPAN." + "Make some menu entries showing proof dependencies of SPAN. +Use `proof-dependency-menu-system-specific' to build system +specific entries." ;; FIXME: might only activate this for dependency-relevant spans. - (list - "-------------" - (proof-dep-make-submenu "Local Dependency..." - (lambda (namespan) (car namespan)) - 'proof-goto-dependency - (span-property span 'dependencies-within-file)) - (proof-make-highlight-depts-menu "Highlight Dependencies" - 'proof-highlight-depcs - span 'dependencies-within-file) - (proof-dep-make-submenu "Local Dependents..." - (lambda (namepos) (car namepos)) - 'proof-goto-dependency - (span-property span 'dependents)) - (proof-make-highlight-depts-menu "Highlight Dependents" - 'proof-highlight-depts - span 'dependents) - ["Unhighlight all" proof-dep-unhighlight t] - "-------------" - (proof-dep-alldeps-menu span))) + (let ((defmenu + (list + "-------------" + (proof-dep-make-submenu "Local Dependency..." + (lambda (namespan) (car namespan)) + 'proof-goto-dependency + (span-property span 'dependencies-within-file)) + (proof-make-highlight-depts-menu "Highlight Dependencies" + 'proof-highlight-depcs + span 'dependencies-within-file) + (proof-dep-make-submenu "Local Dependents..." + (lambda (namepos) (car namepos)) + 'proof-goto-dependency + (span-property span 'dependents)) + (proof-make-highlight-depts-menu "Highlight Dependents" + 'proof-highlight-depts + span 'dependents) + ["Unhighlight all" proof-dep-unhighlight t] + "-------------" + (proof-dep-alldeps-menu span)))) + (if (not proof-dependency-menu-system-specific) + defmenu + (append + (funcall proof-dependency-menu-system-specific span) + defmenu)))) (defun proof-dep-alldeps-menu (span) (or (span-property span 'dependencies-menu) ;; cached value |