diff options
| -rw-r--r-- | CHANGES | 30 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 37 | ||||
| -rw-r--r-- | coq/coq.el | 144 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 33 | ||||
| -rw-r--r-- | generic/proof-config.el | 12 | ||||
| -rw-r--r-- | generic/proof-depends.el | 50 |
6 files changed, 212 insertions, 94 deletions
@@ -47,26 +47,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..e88f9ca8 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 @@ -252,6 +236,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"] @@ -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,120 @@ 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) (not (not deps)))))) + "Coq specific additional menu entry for \"Proof using\". +annotation. See `proof-dependency-menu-system-specific'." ) + +(defun coq-mark-span-dependencies (span suggested) + (goto-char (span-start span)) + (let* ((endpos (re-search-forward "\\<Proof\\(?:\\s-+using\\)?\\>\\([^.]*\\)\\.")) + (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 "\\<Proof\\(?:\\s-+using\\)?\\>\\([^.]*\\)\\."))) + (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..9a3ff12f 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 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 |