From b59f60f9039d58767b6d6f3afb85408d85ccb8a3 Mon Sep 17 00:00:00 2001 From: Axel Daboust Date: Thu, 18 Apr 2024 17:12:19 +0200 Subject: [PATCH] fix issue #605 with coq-specifiq feature --- ci/simple-tests/coq-test-goals-present.el | 279 +++++++++++++++++----- coq/coq.el | 56 +++++ generic/pg-goals.el | 6 +- generic/proof-script.el | 2 + 4 files changed, 282 insertions(+), 61 deletions(-) diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el index e0784f1ba..6ba07db71 100644 --- a/ci/simple-tests/coq-test-goals-present.el +++ b/ci/simple-tests/coq-test-goals-present.el @@ -67,13 +67,33 @@ Proof using. "Coq source code for checking goals after an error.") (defconst coq-src-admitted - "Lemma a : forall(P27X : Prop), P27X. + "Lemma a : forall(P : Prop), P. Proof using. - intros P27X. + intros P. Admitted. " "Coq source for checking that the goals buffer is reset after Admitted.") +(defconst coq-src-no-more-goals + " +Lemma a : 1 + 1 = 2. +Proof using. + simpl. + auto. +" + "Coq source code for checking that the goals buffer is reset when +no goals are left.") + +(defconst coq-src-qed + " +Lemma a : 1 + 1 = 2. +Proof using. + simpl. + auto. +Qed. +" + "Coq source code for checking that the goals buffer is reset after Qed.") + (defconst coq-src-update-goal-after-error " (* code taken from pull request #429 *) @@ -97,6 +117,26 @@ Proof. "Coq source code for checking that goals are updated even in case of error.") +(defconst coq-src-update-goal-after-search + " +Lemma g : 1 + 1 = 2. +Proof using. + simpl. + Search (0 + _). +" + "Coq source code for checking that goals are up-to-date after Search.") + + +(defconst coq-src-update-goal-after-check + " +Lemma h : 1 + 2 = 3. +Proof using. + simpl. + Check plus_O_n. +" + "Coq source code for checking that goals are up-to-date after Check.") + + ;;; utility functions (defun record-buffer-content (buf) @@ -121,10 +161,13 @@ BUF should be a string." ;;; define the tests -(defun goals-after-test (coq-src msg) +(defun goals-after-test (coq-src msg check-response-nonempty) "Test that Proof General shows goals after processing COQ-SRC. Process COQ-SRC in a new buffer in one step and check that the -goals buffer is not empty afterwards." +goals buffer is not empty afterwards. If CHECK-RESPONSE-NONEMPTY +is non-nil, additionally check that the response buffer is +non-empty, i.e., shows some message, and is visible in some +window also in two-pane mode." (message "goals-after-test: Check goals are present after %s." msg) (setq proof-three-window-enable nil) (let (buffer) @@ -139,9 +182,20 @@ goals buffer is not empty afterwards." ;; (record-buffer-content "*goals*") ;; check that there is a goal in the goals buffer - (with-current-buffer "*goals*" + (with-current-buffer proof-goals-buffer (goto-char (point-min)) - (should (looking-at "1 \\(sub\\)?goal (ID")))) + (should (looking-at "1 \\(sub\\)?goal (ID"))) + + (when check-response-nonempty + (message + "goals-after-test: Check response buffer is nonempty after %s." + msg) + (with-current-buffer proof-response-buffer + (should (not (equal (point-min) (point-max))))) + (message + "goals-after-test: Check response buffer is visible after %s." + msg) + (should (get-buffer-window proof-response-buffer)))) ;; clean up (when buffer @@ -149,103 +203,210 @@ goals buffer is not empty afterwards." (set-buffer-modified-p nil)) (kill-buffer buffer))))) +(defun goals-buffer-should-be-empty (pos msg) + "Check that `*goals*' is empty after asserting/retracting to POS. +MSG is only used in a message, it should tell after which action +the goals buffer is expected to be empty." + (message "Check that goals buffer is empty after %s" msg) + (goto-char pos) + (proof-goto-point) + (wait-for-coq) + ;; (record-buffer-content "*coq*") + ;; (record-buffer-content "*goals*") + + ;; check that the goals buffer is empty + (with-current-buffer proof-goals-buffer + (should (equal (point-min) (point-max))))) + +(defun goals-buffer-should-get-reset (coq-src coq-stm msg) + "Check that the goals buffer is reset. +Put the string COQ-SRC into a buffer and assert until the first +occurrence of COQ-STM, which should be a regular expression. At +this point the goals buffer needs to contain something. Then +assert to the end of COQ-SRC and check that the goals buffer has +been reset. MSG is used in messages only. It shouls say after +which action the goals buffer should have been reset." + (message "Check that goals are reset after %s." msg) + (setq proof-three-window-enable nil) + (let (buffer) + (unwind-protect + (progn + (find-file "goals.v") + (setq buffer (current-buffer)) + (insert coq-src) + + ;; First fill the goals buffer by asserting until the line + ;; after the first occurrence of COQ-STM. + + (goto-char (point-min)) + (should (re-search-forward coq-stm nil t)) + (forward-line 1) + (message "*goals* should be non-empty after asserting until after %s" + coq-stm) + (proof-goto-point) + (wait-for-coq) + ;; there should be something in the goals buffer now + (with-current-buffer proof-goals-buffer + (should (not (equal (point-min) (point-max))))) + + (goals-buffer-should-be-empty (point-max) msg)) + + ;; clean up + (when buffer + (with-current-buffer buffer + (set-buffer-modified-p nil)) + (kill-buffer buffer))))) + + (ert-deftest goals-after-proof () "Test goals are present after ``Proof''." :expected-result (if coq--post-v87 :failed :passed) - (goals-after-test coq-src-proof "Proof")) + (goals-after-test coq-src-proof "Proof" nil)) (ert-deftest goals-after-comment () "Test goals are present after a comment." :expected-result :failed - (goals-after-test coq-src-comment "comment")) + (goals-after-test coq-src-comment "comment" nil)) (ert-deftest goals-after-auto () "Test goals are present after ``auto''." :expected-result (if coq--post-v87 :failed :passed) - (goals-after-test coq-src-auto "auto")) + (goals-after-test coq-src-auto "auto" nil)) (ert-deftest goals-after-simpl () "Test goals are present after ``simpl''." - (goals-after-test coq-src-simpl "simpl")) + (goals-after-test coq-src-simpl "simpl" nil)) (ert-deftest goals-after-error () "Test goals are present after an error." :expected-result :failed - (goals-after-test coq-src-error "error")) + (goals-after-test coq-src-error "error" t)) (ert-deftest goals-reset-after-admitted () "The goals buffer is reset after an Admitted." - (message - "goals-reset-after-admitted: Check that goals are reset after Admitted.") - (setq proof-three-window-enable nil) - (let (buffer) - (unwind-protect - (progn - (find-file "goals.v") - (setq buffer (current-buffer)) - (insert coq-src-admitted) - - ;; Need to assert the Admitted alone, therefore first assert - ;; until before the Admitted. - (goto-char (point-min)) - (should (re-search-forward "intros P27X" nil t)) - (forward-line 1) - (proof-goto-point) - (wait-for-coq) - - (forward-line 1) - (proof-goto-point) - (wait-for-coq) - ;; (record-buffer-content "*coq*") - ;; (record-buffer-content "*goals*") - - ;; check that the old goal is not present in the goals buffer - (with-current-buffer "*goals*" - (goto-char (point-min)) - (should (not (re-search-forward "P27X" nil t))))) + (goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted")) - ;; clean up - (when buffer - (with-current-buffer buffer - (set-buffer-modified-p nil)) - (kill-buffer buffer))))) +(ert-deftest goals-reset-no-more-goals () + "The goals buffer is reset when there are no more goals." + (goals-buffer-should-get-reset coq-src-no-more-goals + "Lemma a" "no more goals")) -(ert-deftest update-goals-after-error () - "Test goals are updated after an error." +(ert-deftest goals-reset-qed () :expected-result :failed - (message "update-goals-after-error: Check goals are updated after error") + "The goals buffer is reset after Qed." + (goals-buffer-should-get-reset coq-src-qed + "Proof using" "Qed")) + +(defun update-goals-when-response (coq-src first-pos goal-2nd msg) + "Test goals are up-to-date after an error or a command that produces response. +Process COQ-SRC up to the line after the first match of regular +expression FIRST-POS. At this point the goals buffer should not +be empty. Process now COQ-SRC up to the end. If GOAL-2ND is a +regular expression as a string, then check that the goals have +been updated to contain a match for GOAL-2ND. If GOAL-2ND is no +string, only check that the goals buffer is non-empty. In any +case, check that the response buffer is not empty and visible in +two-pane mode." + + (message "update-goals-when-response: Check goals are updated after %s" msg) (setq proof-three-window-enable nil) (let (buffer) (unwind-protect (progn (find-file "goals.v") (setq buffer (current-buffer)) - (insert coq-src-update-goal-after-error) + (insert coq-src) (goto-char (point-min)) - (should (re-search-forward "point A" nil t)) - (beginning-of-line) + (should (re-search-forward first-pos nil t)) + (forward-line 1) (proof-goto-point) (wait-for-coq) ;; (record-buffer-content "*coq*") ;; (record-buffer-content "*goals*") - ;; the complete goal should be present - (with-current-buffer "*goals*" - (goto-char (point-min)) - (should (re-search-forward "(eq_one 1 -> False) -> False" nil t))) + ;; goals should be present + (message "Check that goals are present") + (with-current-buffer proof-goals-buffer + (should (not (equal (point-min) (point-max))))) - (should (re-search-forward "point B" nil t)) - (beginning-of-line) + (goto-char (point-max)) (proof-goto-point) (wait-for-coq) ;; (record-buffer-content "*coq*") ;; (record-buffer-content "*goals*") - ;; the hypothesis H should be present - (with-current-buffer "*goals*" + (with-current-buffer proof-goals-buffer (goto-char (point-min)) - (should (re-search-forward "H : eq_one 1 -> False" nil t)))) + (if (stringp goal-2nd) + (progn + (message "Check that goals have been updated") + (should (re-search-forward goal-2nd nil t))) + (message "Check that goals are still present") + (should (not (equal (point-min) (point-max)))))) + + ;; something should be in the response buffer + (message "Check that there is some response present") + (with-current-buffer proof-response-buffer + (should (not (equal (point-min) (point-max))))) + + (message "Check that the response is visible in two-pane mode") + (should (get-buffer-window proof-response-buffer))) + (when buffer (with-current-buffer buffer (set-buffer-modified-p nil)) (kill-buffer buffer))))) + +(ert-deftest goals-up-to-date-at-error () + "Check that goals are updated before showing the error." + :expected-result :failed + (update-goals-when-response coq-src-update-goal-after-error + "Lemma foo" + "H : eq_one 1 -> False" + "error")) + +(ert-deftest goals-up-to-date-after-search-one-step () + "Check that goals are still present before showing result of one search cmd. +This test checks a single Search command inside a proof. After +processing that Search command alone, the goals buffer should not +be empty and the response buffer should contain something and be +visible in two-pane mode." + (update-goals-when-response coq-src-update-goal-after-search + "simpl" + t + "Search")) + +(ert-deftest goals-updated-after-search-many-steps () + "Check that goals are updated before showing result of search cmd. +This test checks several commands inside a proof with a final +Search command. After processing these commands, the goals buffer +should have been updated and the response buffer should contain +something and be visible in two-pane mode." + :expected-result :failed + (update-goals-when-response coq-src-update-goal-after-search + "Lemma g" + "2 = 2" + "Search")) + +(ert-deftest goals-up-to-date-after-check-one-step () + "Check that goals are still present before showing result of one check cmd. +This test checks a single Check command inside a proof. After +processing that Check command alone, the goals buffer should not +be empty and the response buffer should contain something and be +visible in two-pane mode." + (update-goals-when-response coq-src-update-goal-after-check + "simpl" + t + "Check")) + +(ert-deftest goals-updated-after-check-many-steps () + "Check that goals are updated before showing result of check cmd. +This test checks several commands inside a proof with a final +Check command. After processing these commands, the goals buffer +should have been updated and the response buffer should contain +something and be visible in two-pane mode." + :expected-result :failed + (update-goals-when-response coq-src-update-goal-after-check + "Lemma h" + "3 = 3" + "Check")) diff --git a/coq/coq.el b/coq/coq.el index a036acde3..8f7a18a4a 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1261,6 +1261,62 @@ width is synchronized by coq (?!)." :safe 'booleanp :group 'coq) +;; update *goals* buffer modeline +(defun coq-parse-goals-info (goals-output) + "Parse output to extract and update goals information in modeline." + (let ((goals-count-regexp "^\\([0-9]+\\) goals? (ID \\([0-9]+\\))") + (num-goals 0) + (current-goal-id nil)) + (when (string-match goals-count-regexp goals-output) + (setq num-goals (string-to-number (match-string 1 goals-output))) + (setq current-goal-id (match-string 2 goals-output))) + (update-goals-modeline num-goals current-goal-id) + ; hide goals info on first line + (with-current-buffer proof-goals-buffer + (goto-char (point-min)) + (let ((line-end (line-end-position))) + (let ((overlay (make-overlay (point-min) line-end))) + ; invisible line + (overlay-put overlay 'invisible t)))))) + +(defun update-goals-modeline (goal id) + "Extracts proof state and updates the goals buffer modeline dynamically." + (with-current-buffer proof-goals-buffer + (let ((goal-str (if (> goal 1) "goals" "goal"))) + (setq-local my-goals-info + (format "%d %s, ID: %s" goal goal-str id))) + (let ((baseline-mode-line-format + '("%e" + mode-line-front-space + mode-line-mule-info + mode-line-client + mode-line-modified + mode-line-remote + mode-line-frame-identification + mode-line-buffer-identification + " " + mode-line-position + " " + mode-line-modes + mode-line-misc-info + mode-line-end-spaces))) + + (setq-local mode-line-format + (append baseline-mode-line-format + `((" " (:eval my-goals-info))))) ; update + + (force-mode-line-update)))) + +(defun reset-goals-modeline () + "Resets the *goals* buffer modeline to indicate no active proof." + (with-current-buffer proof-goals-buffer + (setq-local my-goals-info "") + (setq-local mode-line-format + (append + '("%e" mode-line-front-space mode-line-mule-info mode-line-client mode-line-modified mode-line-remote mode-line-frame-identification mode-line-buffer-identification " " mode-line-position " " mode-line-modes mode-line-misc-info mode-line-end-spaces) + `((" " (:eval my-goals-info))))) + (force-mode-line-update))) + (defvar coq-shell-current-line-width nil "Current line width of the Coq printing width. Its value will be updated whenever a command is sent if diff --git a/generic/pg-goals.el b/generic/pg-goals.el index f7cb9b3c7..14891709f 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -107,8 +107,10 @@ so the response buffer should not be cleared." (bufhist-checkpoint-and-erase)) ;; Only display if string is non-empty. - (unless (string-equal string "") - (funcall pg-insert-text-function string)) + (when (not (string-equal string "")) + (funcall pg-insert-text-function string) + (when (string-equal proof-assistant "Coq") + (coq-parse-goals-info string))) (setq buffer-read-only t) (set-buffer-modified-p nil) diff --git a/generic/proof-script.el b/generic/proof-script.el index 854bd6bf8..d3de7ac00 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1486,6 +1486,8 @@ Besides stuff that is not yet documented here, this function and sections. - enters some commands and their spans in some database (with for me unknown purpose)" + (when (string-equal proof-assistant "Coq") + (reset-goals-modeline)) ; Erase goal modeline when a proof is closed (unless (or (eq proof-shell-proof-completed 1) ;; (eq proof-assistant-symbol 'isar) )