diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 61c979fb6..5a5f29415 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -202,7 +202,7 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 020_coq-test-definition () ;; There are no infomsgr when running silent. - :expected-result :failed + :expected-result (if (coq--version< (coq-version) "9.2alpha") :failed :passed) "Test *response* output after asserting a Definition." (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") @@ -401,7 +401,7 @@ For example, COMMENT could be (*test-definition*)" ;; When running silent, the message about indeed failing is not ;; shown. One might fix this test by checking that there is no ;; error, which would be shown without Fail. - :expected-result :failed + :expected-result (if (coq--version< (coq-version) "9.2alpha") :failed :passed) "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") @@ -429,7 +429,7 @@ For example, COMMENT could be (*test-definition*)" ;; When running silent, the message about indeed failing is not ;; shown. One might fix this test by checking that there is no ;; error, which would be shown without Fail. - :expected-result :failed + :expected-result (if (coq--version< (coq-version) "9.2alpha") :failed :passed) "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") diff --git a/ci/test.sh b/ci/test.sh index 50d075798..6805337f0 100755 --- a/ci/test.sh +++ b/ci/test.sh @@ -36,4 +36,5 @@ form="(progn (add-to-list 'load-path \"$rootdir\") (add-to-list 'load-path \"$srcdir\") (setq coq-test-dir \"$srcdir/\"))" # we need a trailing slash here + assert emacs --batch -l ert --eval "$form" -l init-tests.el -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit diff --git a/coq/coq-system.el b/coq/coq-system.el index e9b3acd7f..d0d738f3b 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -150,7 +150,10 @@ This function must not rely on coq-autodetect-version, it would be a cycle." (with-temp-buffer (setq retv (apply 'process-file process-args)) (if (or (not expectedretv) (equal retv expectedretv)) (buffer-string))) - (error nil)))) + (error + (message "Warning: No Coq/Rocq version detected yet.") + (message "ProofGeneral will not be able to start a prover session until you have one in your path.") + nil)))) (defun coq-autodetect-version (&optional interactive-p) "Detect and record the version of Coq currently in use. @@ -171,12 +174,13 @@ Interactively (with INTERACTIVE-P), show that number." (setq coq-autodetected-help (or coq-output "")))) (defun coq--version< (v1 v2) - "Compare Coq versions V1 and V2." + "Compare Coq versions V1 and V2. +If V1 or V2 is not a valid version number, return nil." ;; -snapshot is only supported by Emacs 24.5, not 24.3 (let ((version-regexp-alist `(("^[-_+ ]?snapshot$" . -4) ("^pl$" . 0) ,@version-regexp-alist))) - (version< v1 v2))) + (condition-case nil (version< v1 v2) (error nil)))) (defcustom coq-pre-v85 nil "Deprecated. diff --git a/coq/coq.el b/coq/coq.el index f9b25eae2..b7aedf90d 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -141,7 +141,10 @@ Namely, goals that do not fit in the goals window." ;; keeping the current value (that may come from another file). ,(format "Add Search Blacklist %s." coq-search-blacklist-current-string)) '("Set Suggest Proof Using.") - (if coq-run-completely-silent '("Set Silent.") ()) + (if (and coq-run-completely-silent + (coq--version< (coq-version t) "9.2+alpha")) + '("Set Silent.") + ()) coq-user-init-cmd) "Commands for initial Coq configuration, Coq variant of `proof-shell-init-cmd'. List of commands sent to the Coq background process just after it @@ -381,27 +384,55 @@ It is mostly useful in three window mode, see also ;; result, if it follows we want it to be non urgent, otherwise the result ;; would not be shown in response buffer. If it is before, then we want it ;; urgent so that it is displayed. -(defvar coq-eager-no-urgent-regex "\\s-*Finished " +(defvar coq-eager-no-urgent-regex + ;; "\\s-*Finished \\|" not needed anymore in silent mode (and in roc W= 9.2, + ;; since the goal is not printed in the same command (but by the next Show). + ;; TODO: remove it after a few versions. + "\\s-*Finished \\|\n?\\s-*This subproof is complete, but\\|\\s-*All the remaining goals are on the shelf." "Regexp of commands matching `proof-shell-eager-annotation-start' that should maybe not be classified as urgent messages.") +(defconst coq--goal-header--when-unfocused-goals "[0-9]+ goals?\n\ngoal ";; The trailing white space is important here + "Regexp for goals displyed when there are no focused goal. + +This regexp should match the start of coq's goal printing ONLY when there +is currently no goal under focus. This is used in +`coq-non-urgent-eager-annotation` to detect a infomsg that should NOT be +considered urgent: (because we only want it displayed for the last +command).") + + ;; return the end position if found, nil otherwise (defun coq-non-urgent-eager-annotation () + "Return non-nil if looking at a non-urgent eager annotation. + +See `coq-search-urgent-message'." (save-excursion - (when (and (looking-at coq-eager-no-urgent-regex) - (re-search-forward proof-shell-eager-annotation-end nil t)) - (let ((res (match-end 0))); robustify - ;; if there is something else than a prompt here then this eager - ;; annotation is left urgent (return nil), otherwise it is not urgent - ;; (return position of the end of the annotation) - (when (looking-at (concat "\\s-*" proof-shell-annotated-prompt-regexp)) - res))))) + (if (looking-at coq-eager-no-urgent-regex) + (if (re-search-forward proof-shell-eager-annotation-end nil t) + (let ((res (match-end 0))); robustify + ;; if there is something else than a prompt (????or an unfocused goal?) here then this eager + ;; annotation is left urgent (return nil), otherwise it is not urgent + ;; (return position of the end of the annotation) + (when (or (looking-at (concat "\\s-*" proof-shell-annotated-prompt-regexp)) + (looking-at (concat "\\s-*" coq--goal-header--when-unfocused-goals))) + res)) + t) + nil))) ;; Looking for eager annotation which does not match coq-eager-no-urgent-regex (defun coq-search-urgent-message () - "Find forward the next really urgent message. + "Find forward next eager annotation that is really urgent. + Return the position of the beginning of the message (after the -annotation-start) if found." +annotation-start) if found. + +This function is used in Coq's replacement for +`proof-shell-process-urgent-messages'. It replaces a simple search +`proof-shell-eager-annotation-start' because some messages that do match +it should not be treated as urgent. This is due to a mismatch between +message category between Coq and PG. +" (let ((again t) (start-start nil) (end-end nil) ;; (found nil) (eager proof-shell-eager-annotation-start)) (while again @@ -429,7 +460,46 @@ between regexps `proof-shell-eager-annotation-start' and We update `proof-shell-urgent-message-marker' to point to last message found. -This is a subroutine of `proof-shell-filter'." +This is a subroutine of `proof-shell-filter'. + +DOCUMENTATION OF THIS VERSION OF THE FUNCTION (redefined for Coq). + +When thi shappens: + + PROMPT-0 > command1. + MESSAGE-1 + PROMPT-1 > command2. + MESSAGE-2 + GOALS-2 + PROMPT-2 > + +MESSAGE-2 is displayed. Even if it is urgent because it concerns the +last command. + +But (non urgent) MESSAGE-1 is not displayed by default. There is only +one case where MESSAGE-1 is displayed: if both following conditions are +true. + +- command2 is inserted in action-list with the 'keep-response tag +- AND MESSAGE-2 (not MESSAGE-1) IS NOT URGENT. + +Thus we detect cases where we want MESSAGE-2, despite being an eager +annotation, shoudl not be considered urgent. + +One such situation comes from the fact that PG now systematically +inserts a \"Show\" command at the end of the action-list. So now we have +this: + + PROMPT-0 <= last command2 + MESSAGE-1 + PROMPT-1 <= Show. + MESSAGE-2 + GOALS-2 + PROMPT-2 > + +And we want MESSAGE-1 to be visible together with MESSAGE-2 (which can +be something like \"This subproof is complete, but ...\"). +" (let ((pt (point)) (end t) lastend laststart (initstart (max (marker-position proof-shell-urgent-message-scanner) @@ -2461,6 +2531,23 @@ Return command that undos to state." (defconst coq--time-prefix "Time " "Coq command prefix for displaying timing information.") +(defconst coq--non-timeable-command-regexp "\\`BackTo" + "Regexp for Coq (non bullet) commands not supporting \"Time\". + +See `coq-cmd-incompatible-with-Time'. ") + +(defun coq-cmd-incompatible-with-Time (str) + "Return non-nil if str is a command that support Time. + +Time CMD. is supposed to execute CMD and then print the cpu time it took +to execute. It is not applicable to commands like e.g. \"BackTo\" or +bullets. + +Uses `coq--non-timeable-command-regexp`. +" + (or (coq-bullet-p str) ;; coq does not accept "Time -". + (string-match coq--non-timeable-command-regexp str))) + (defun coq-bullet-p (s) (string-match coq-bullet-regexp-nospace s)) @@ -2470,7 +2557,8 @@ Return command that undos to state." (with-no-warnings ;; NB: dynamic scoping of `string' and `action' ;; Don't add the prefix if this is a command sent internally (unless (or (eq action 'proof-done-invisible) - (coq-bullet-p string)) ;; coq does not accept "Time -". + ;; Some cmds do not support "Time". + (coq-cmd-incompatible-with-Time string)) (setq string (concat coq--time-prefix string)) ;; coqtop *really wants* a newline after a comand-ending dot. ;; (error) locations are very wrong otherwise diff --git a/generic/proof-shell.el b/generic/proof-shell.el index cf8a2abce..a4f30076b 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1788,7 +1788,13 @@ by the filter is to send the next command from the queue." "If FLAGS permit, display response STR; set `proof-shell-last-response-output'." (setq proof-shell-last-response-output str) ; set even if not displayed (unless (memq 'no-response-display flags) - (pg-response-display str))) + ;; if keep-response then we do not really erase the response + ;; (hence the fourth arg), but we still want to update + ;; pg-response-erase-flag correctly + (pg-response-maybe-erase t nil nil (member 'keep-response flags)) + (pg-response-display-with-face str) + (proof-display-and-keep-buffer proof-response-buffer))) + (defun proof-shell-handle-delayed-output () "Display delayed goals/responses, when queue is stopped or completed.