Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coq: run silently and explicitly Show when necessary #742

Closed
wants to merge 5 commits into from
Closed

coq: run silently and explicitly Show when necessary #742

wants to merge 5 commits into from

Commits on Apr 7, 2024

  1. coq: run silently and explicitly Show when necessary 

    This is a step towards fixing ProofGeneral#568. It fixes the cases after Proof,
comments and auto, leaving now 3 instead of 6 failing tests in
ci/simple-tests/test-goals-present.el.
    @hendriktews
    hendriktews committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    b984de6 View commit details
    Browse the repository at this point in the history

  2. fix tests for preceding commit 

    - update manuals
- expect test goals-reset-after-admitted to fail again
- expect errors in tests 020_coq-test-definition,
  090_coq-test-regression-Fail and 091_coq-test-regression-Fail
    @hendriktews
    hendriktews committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    2d307a6 View commit details
    Browse the repository at this point in the history

  3. CI test-goals-present: two more tests for resetting the goals buffer 

    - goals should be reset when there are no more goals (does work)
- goals should be reset after Qed (does not work)
    @hendriktews
    hendriktews committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    1414157 View commit details
    Browse the repository at this point in the history

  4. CI: extend goals present tests to check for errors if applicable 

    Extend the goals present tests to additionally check that the response
buffer contains some text (i.e., an error message) in those cases
where an error is expected.
    @hendriktews
    hendriktews committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    fb442fd View commit details
    Browse the repository at this point in the history

  5. coq: fix goals update after error 

    This commit fixes two more cases of ProofGeneral#568: The goals buffer is updated
in case of an error if Coq is inside a proof. Care is taken to keep
the error message in the response buffer and to show the response
buffer in two-pane mode.

The fix works by issuing a Show command as a priority action item from
proof-shell-handle-error-or-interrupt-hook, which runs at the end of
the error processing. The new action item flag 'keep-response tells
the generic machinery to not clear the response buffer and to keep it
in two-pane mode.
    @hendriktews
    hendriktews committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    0b42f93 View commit details
    Browse the repository at this point in the history