From d1053a06aa31ce05fa0741fb61dfb1266fcb0364 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 10 Apr 2020 13:08:29 +0200 Subject: Fixed proof using annotation mechanism. I ended up using (in a slight devious way) the lemma dependency mechanism of PG: the dependency information stored in the span is only the ones suggested by coq: only the one that should appear in theproof using annotation (and only when coq felt the need to suggest them. --- coq/coq.el | 63 ++++++++++++++++++++---------------------------- generic/proof-config.el | 7 ++++++ generic/proof-depends.el | 3 ++- 3 files changed, 35 insertions(+), 38 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 48be8f37..8b427ecf 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1937,6 +1937,7 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-shell-error-regexp coq-error-regexp proof-shell-interrupt-regexp coq-interrupt-regexp proof-shell-assumption-regexp coq-id + proof-shell-theorem-dependency-list-regexp coq-shell-theorem-dependency-list-regexp pg-subterm-first-special-char ?\360 ;; The next three represent path annotation information pg-subterm-start-char ?\372 ; not done @@ -2558,6 +2559,9 @@ Warning: this makes the error messages (and location) wrong.") ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; +(setq coq-shell-theorem-dependency-list-regexp + "\\(?: \\|\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." @@ -2567,56 +2571,41 @@ recieving suggestions from coq at Qed time." (const :tag "never accept" never)) :group 'coq) -(defun coq-extract-proof-using-from-suggestion () - (proof-with-current-buffer-if-exists proof-response-buffer - (when (string-match - "following commands:\n.*Proof using\\([^.]*\\)\\." - (buffer-string)) - (let* ((s (match-string 1 (buffer-string))) - (prefix (if (equal (aref s 0) ? ) " using" " using "))) - (concat prefix s))))) - -(defun coq-proof-using-equal (s1 s2) - (let* ((l1 (split-string s1)) (l2 (split-string s2)) - (diff (cl-set-exclusive-or l1 l2 :test 'string-equal))) - (not diff))) ;; nil if empty xor - +(defun coq-extract-proof-using-from-suggestion (span) + (let ((sp (span-property-safe span 'dependencies))) + sp)) -(defun coq-insert-proof-using-suggestion (suggested) - ;; Not compatible with nested lemmas. +(defun coq-insert-proof-using-suggestion (span suggested) + "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 (proof-unprocessed-begin)) + (goto-char (span-start span)) (let* ((pos-unproc (point)) - (proof-pos (save-excursion - (search-backward-regexp "\\\\([^.]*\\)\\."))) - (previous-content (match-string 1)) - (same (coq-proof-using-equal previous-content suggested))) - (when (and (not same) (or (equal coq-accept-proof-using-suggestion 'always) - (y-or-n-p (concat "Update proof using annotation (" - suggested ")")))) + (endpos (save-excursion + (search-forward-regexp "\\\\([^.]*\\)\\."))) + (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) + (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 suggested) + (insert (concat " using " string-suggested)) ;; go back to `proof-strict-read-only' says (proof-span-read-only spl))))))) -;; This should be called after a Save or Qed command is called (but not a -;; "Define"). -(defun coq-proof-using-suggest-hook () - (unless (equal coq-accept-proof-using-suggestion 'never) - (let ((suggestion (coq-extract-proof-using-from-suggestion))) - (when suggestion - (coq-insert-proof-using-suggestion suggestion))))) - - -;(add-hook 'proof-shell-handle-delayed-output-hook - ;#'coq-proof-using-suggest-hook t) - +(defun proof-dependencies-system-specific (name span) + (let ((suggested (coq-extract-proof-using-from-suggestion span))) + (coq-insert-proof-using-suggestion span suggested))) ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; diff --git a/generic/proof-config.el b/generic/proof-config.el index f9947757..41c5e9d7 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1758,6 +1758,13 @@ This hook is used within Proof General to refresh the toolbar." :type '(repeat function) :group 'proof-shell) +;;;;;; +(defcustom proof-dependencies-system-specific nil + "doc TODO" + :type '(repeat function) + :group 'proof-shell) +;;;;; + (defcustom proof-shell-syntax-table-entries nil "List of syntax table entries for proof script mode. A flat list of the form diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 163a0968..c3de97f7 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -120,7 +120,8 @@ Called from `proof-done-advancing' when a save is processed and 'type)))) (span-set-property gspan 'dependencies-within-file depspans) - (setq proof-last-theorem-dependencies nil))) + (setq proof-last-theorem-dependencies nil) + (funcall 'proof-dependencies-system-specific name gspan))) -- cgit v1.2.3