Coq: run silently and explicitly Show when necessary - second attempt #762
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hendriktews
force-pushed
the
silent-2
branch
3 times, most recently
from
b7cb334
to
0758343
Compare
This is a step towards fixing ProofGeneral#568. It fixes the cases after Proof, comments, auto, errors, Search and Check, leaving now 2 instead of 8 failing tests in ci/simple-tests/test-goals-present.el. Admitted is not handled correctly any more, which is a regression. Using proof-shell-handle-delayed-output-hook and proof-shell-handle-error-or-interrupt-hook we issue a Show command as a priority action item when the last (normal) action item has been processed. The new action item flag 'keep-response tells the generic machinery to not clear the response buffer and to keep it present in two-pane mode in case an error was detected or the last command was a Search or Check that produced a response. The new action item flag 'dont-show-when-silent is used to distinguish the additional Show commands and to avoid an endless loop of Show commands. Set proof-shell-last-output-kind now in proof-shell-handle-delayed-output such that it correctly reflects the cases of goals and response (which has not been the case since commit 037dc9b from 2009. This commit breaks coq-show-proof-stepwise to some extend. Expect 080_coq-test-regression-show-proof-stepwise to fail. Additionally: - update manuals - expect errors in tests 020_coq-test-definition, 090_coq-test-regression-Fail and 091_coq-test-regression-Fail because messages are not printed in silent mode
This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.
Add user option coq-run-completely-silent, which, when disabled, switches Coq to old behavior where Coq is dynamically switched to silent on longer action item lists.
|
@Matafou , @erikmd , @cpitclaudel : With the option |
|
Hi @hendriktews! (I just quickly skimmed the PR code but) LGTM, thanks.
Agree |
|
Maybe I need to test how it interacts with debug mode. I don't have much time this week though. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is another attempt towards fixing #568.