fix issue ProofGeneral#605

ci/doc/currently-used-coq-emacs-versions

@@ -14,27 +14,27 @@ coq-8.14.1-emacs-26.3
 coq-8.14.1-emacs-27.1
 coq-8.14.1-emacs-27.2
 coq-8.14.1-emacs-29.2
-coq-8.15.1-emacs-26.3
-coq-8.15.1-emacs-27.1
-coq-8.15.1-emacs-27.2
-coq-8.15.1-emacs-28.1
-coq-8.15.1-emacs-28.2
-coq-8.15.1-emacs-29.1
-coq-8.15.1-emacs-29.2
+coq-8.15.2-emacs-26.3
+coq-8.15.2-emacs-27.1
+coq-8.15.2-emacs-27.2
+coq-8.15.2-emacs-28.1
+coq-8.15.2-emacs-28.2
+coq-8.15.2-emacs-29.1
+coq-8.15.2-emacs-29.2
 coq-8.16.1-emacs-26.3
 coq-8.16.1-emacs-27.1
 coq-8.16.1-emacs-27.2
 coq-8.16.1-emacs-28.1
 coq-8.16.1-emacs-28.2
 coq-8.16.1-emacs-29.1
 coq-8.16.1-emacs-29.2
-coq-8.17.0-emacs-26.3
-coq-8.17.0-emacs-27.1
-coq-8.17.0-emacs-27.2
-coq-8.17.0-emacs-28.1
-coq-8.17.0-emacs-28.2
-coq-8.17.0-emacs-29.1
-coq-8.17.0-emacs-29.2
+coq-8.17.1-emacs-26.3
+coq-8.17.1-emacs-27.1
+coq-8.17.1-emacs-27.2
+coq-8.17.1-emacs-28.1
+coq-8.17.1-emacs-28.2
+coq-8.17.1-emacs-29.1
+coq-8.17.1-emacs-29.2
 coq-8.18.0-emacs-26.3
 coq-8.18.0-emacs-27.1
 coq-8.18.0-emacs-27.2

ci/doc/currently-used-coq-nix-versions

@@ -5,8 +5,8 @@
 8.12.2
 8.13.2
 8.14.1
-8.15.1
+8.15.2
 8.16.1
-8.17.0
+8.17.1
 8.18.0
 8.19.1

ci/simple-tests/coq-test-goals-present.el

@@ -174,7 +174,6 @@ goals buffer is not empty afterwards."
   (goals-after-test coq-src-error "error"))
 
 (ert-deftest goals-reset-after-admitted ()
-  :expected-result :failed
   "The goals buffer is reset after an Admitted."
   (message
    "goals-reset-after-admitted: Check that goals are reset after Admitted.")

ci/simple-tests/coq-test-omit-proofs.el

@@ -92,10 +92,11 @@ configured there may be taken from faces with less priority."
   "Test the omit proofs feature.
 In particular, test that with proof-omit-proofs-option configured:
 - the proof _is_ processed when using a prefix argument
-- in this case the proof as normal locked color
+- in this case the proof has normal locked color
 - without prefix arg, the proof is omitted
 - the proof has omitted color then
 - stuff before the proof still has normal color "
+  (message "omit-proofs-omit-and-not-omit: Check several omit proofs features")
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
   (reset-coq)
@@ -154,10 +155,21 @@ In particular, test that with proof-omit-proofs-option configured:
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
-  (with-current-buffer "*response*"
-    (goto-char (point-min))
-    ;; There should be a declared message.
-    (should (looking-at "classic_excluded_middle is declared")))
+  (with-current-buffer "*coq*"
+    ;; There should be an Admit at the second last prompt without error.
+    (goto-char (point-max))
+    (should (search-backward "</prompt>" nil t 2))
+    ;; move behind prompt
+    (forward-char 9)
+    (should (looking-at "Admitted\\.\n"))
+    (forward-line 1)
+    ;; There may be an info message about the declaration. The message
+    ;; may be spread over several lines.
+    (when (looking-at "<infomsg>")
+      (should (search-forward "</infomsg>" nil t))
+      (forward-line 1))
+    ;; no other messages or errors before the next prompt
+    (should (looking-at "\n<prompt>Coq <")))
 
   ;; Check 4: check proof-omitted-proof-face is active at marker 3
   (message "4: check proof-omitted-proof-face is active at marker 3")
@@ -184,6 +196,7 @@ the normal `proof-locked-face'.
 
 The sources for the test contain a local attribute in form of
 '#[local]', which has been introduced only in Coq version 8.9."
+  (message "omit-proofs-never-omit-hints: Check omit proofs feature with Hint")
   (skip-unless coq--post-v809)
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
@@ -206,6 +219,7 @@ Test that proofs for Let local declarations are never omitted and
 that proofs of theorems following a Let definition are omitted.
 
 This test only checks the faces in the middle of the proof."
+  (message "omit-proofs-never-omit-lets: Check omit proofs feature with Let")
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
   (reset-coq)

ci/tools/cipg.ml

@@ -1588,7 +1588,6 @@ let main() =
             end
           else
             print_endline"\n\nno superfluous container to delete\n";
-          update_currently_used coqs (list_of_matrix coqs emacses conts);
         end;
     end;
   if !print_pg_ci_config then
@@ -1641,6 +1640,8 @@ let main() =
 
       yml_file_change_wrapper test_workflow_file "magic-emacs-version"
         (output_ci_magic_versions latest_two_emacs_major);
+
+      update_currently_used coqs (list_of_matrix coqs emacses conts);
     end;
   ()
 

coq/coq.el

@@ -145,8 +145,20 @@ Namely, goals that do not fit in the goals window."
 ;;  "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists).
   "*Command of the inferior process to change the directory.")
 
-(defvar coq-shell-proof-completed-regexp "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|Proof\\s-completed"; \\|This subproof is complete
-  "*Regular expression indicating that the proof has been completed.")
+(defvar coq-shell-proof-completed-regexp
+  (concat "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|"
+          "Proof\\s-completed\\|"
+          ;; if printing width is small, eg. when running in batch mode,
+          ;; there might be a line break after infomsg
+          "<infomsg>\n?.*\\s-is\\s-declared"
+          ;; \\|This subproof is complete
+          )
+  "*Regular expression indicating that the proof has been completed.
+Coq instance of `proof-shell-clear-goals-regexp'. Used in
+`proof-shell-process-urgent-message' to determine if the goals
+buffer shall be cleaned. Some of the messages recognized here are
+not printed by Coq in silent mode, such that Proof General might
+fail to delete the goals buffer.")
 
 (defvar coq-goal-regexp
   "\\(============================\\)\\|\\(\\(?:sub\\)?goal [0-9]+\\)\n")

generic/pg-goals.el

@@ -79,6 +79,63 @@ May enable proof-by-pointing or similar features.
 ;;
 ;; Goals buffer processing
 ;;
+
+;; 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)))
+
 (defun pg-goals-display (string keepresponse)
   "Display STRING in the `proof-goals-buffer', properly marked up.
 Converts term substructure markup into mouse-highlighted extents.
@@ -107,8 +164,9 @@ 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)
+      (coq-parse-goals-info string))
 
     (setq buffer-read-only t)
     (set-buffer-modified-p nil)

generic/proof-script.el

@@ -1486,6 +1486,7 @@ 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)"
+  (reset-goals-modeline) ; Erase goal buffer when a proof is closed
   (unless (or (eq proof-shell-proof-completed 1)
 	      ;; (eq proof-assistant-symbol 'isar)
 	      )

generic/proof-shell.el

@@ -35,6 +35,7 @@
 ;;   proof-shell-filter-wrapper
 ;;   -> proof-shell-filter
 ;;      -> proof-shell-process-urgent-messages
+;;         -> proof-shell-process-urgent-message
 ;;      -> proof-shell-filter-manage-output
 ;;         -> proof-shell-handle-immediate-output
 ;;         -> proof-shell-exec-loop