From ea935933491b7a89ea27685aab3af5eb7d7288c0 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 11 Nov 2025 11:00:29 +0100 Subject: [PATCH] Rocq: enable messages for Rocq >= 9.2 Disable Set Silent for Rocq >= 9.2, which does not print any goals any more. See also PR 21038 for Rocq. Fixes #842 #849 #843 --- ci/coq-tests.el | 6 +++--- coq/coq.el | 5 ++++- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 61c979fb6..c6c466854 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 :failed "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 :failed "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 :failed "Test for Fail" (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") diff --git a/coq/coq.el b/coq/coq.el index 0fc0222fb..ce60a21eb 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