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

Why does PG show stale goals? #568

Open
cpitclaudel opened this issue Mar 30, 2021 · 7 comments
Open

Why does PG show stale goals? #568

cpitclaudel opened this issue Mar 30, 2021 · 7 comments
Labels
kind: bug kind: question kind: regression

Comments

@cpitclaudel
Copy link
Member

I don't know what happened of late, but over the last few years it's become more and more common that I have to ask PG to refresh the goal explicitly. Often the goal window stays blank, or it shows an outdated goal. If a comment follows a bit of code and both are processed together, PG doesn't show the goal. And so on.

What's going on? It's come to the point that C-c C-p is one of the first PG keybindings I teach my students. Is it our fault, or is it on Coq's side?
@hendriktews
Copy link
Collaborator

I would say it is the silent processing together with the difficulty to reliably insert something in proof-action-list. I believe it is our fault. With 8d545bc and 14ea1a3 it will become easier to insert stuff into proof-action-list.

@cpitclaudel
Copy link
Member Author

Thanks. Then I think we should treat your work as critical-priority. At the moment, PG is basically unusable for newcomers. Teaching a Coq class is a real reality check on that front.

@Matafou
Copy link
Contributor

Matafou commented Apr 2, 2021

It is our fault for sure, but it also comes from coq slowly changing its behaviour. I think it spontaneously prints the goal less often. We definitely need to refactor the "Show" stuff.

@Matafou
Copy link
Contributor

Matafou commented Apr 2, 2021

@hendriktews is it really a problem of adding to the action list? It looks to me that we need a way to issue a "Goal" precisely when there is nothing left in the action list (and there is an open proof). Without cleaning the response buffer.

@cpitclaudel
Copy link
Member Author

Thanks @Matafou.

@erikmd erikmd mentioned this issue Apr 15, 2021
Merged
hendriktews added a commit to hendriktews/PG that referenced this issue Jun 6, 2021
@hendriktews
add tests for checking that goals are correctly shown
ae22919 
Most of these tests currently fail because of different instances
of ProofGeneral#568, see also ProofGeneral#429, ProofGeneral#467.
@hendriktews hendriktews mentioned this issue Jun 6, 2021
Merged
@hendriktews
Copy link
Collaborator

hendriktews commented Jun 6, 2021 •
edited
Loading

I opened a PR with tests where PG does not show any goal or the wrong one. They cover the cases of

  • Proof
  • comment at the end of the queue region
  • auto
  • error in the proof script

If you know another way to get no or the wrong goal in PG, please add a test or tell here about it.

@ejgallego
Copy link

This is likely due coqtop not printing a goal again if it didn't change. For example, after Proof..

Only reliable fix is to actually move to a model where PG queries for goals, and stops playing weird games with Coq output [ PG will always lose]

@ejgallego ejgallego mentioned this issue Nov 3, 2021
Open
@Matafou Matafou mentioned this issue Jan 10, 2023
Closed
hendriktews added a commit to hendriktews/PG that referenced this issue Jan 23, 2024
@hendriktews
add tests for checking that goals are correctly shown
f0ccaf8 
Most of these tests currently fail because of different instances
of ProofGeneral#568, see also ProofGeneral#429, ProofGeneral#467, ProofGeneral#103.
hendriktews added a commit to hendriktews/PG that referenced this issue Jan 28, 2024
@hendriktews
add tests for checking that goals are correctly shown
410d1d9 
Most of these tests currently fail because of different instances
of ProofGeneral#568, see also ProofGeneral#429, ProofGeneral#467, ProofGeneral#103.
hendriktews added a commit to hendriktews/PG that referenced this issue Feb 7, 2024
@hendriktews
add tests for checking that goals are correctly shown
3fd2d96 
Most of these tests currently fail because of different instances
of ProofGeneral#568, see also ProofGeneral#429, ProofGeneral#467, ProofGeneral#103.
hendriktews added a commit that referenced this issue Feb 18, 2024
@hendriktews
add tests for checking that goals are correctly shown
a6bd818 
Most of these tests currently fail because of different instances
of #568, see also #429, #467, #103.
hendriktews added a commit to hendriktews/PG that referenced this issue Mar 2, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
d8fd9c4 
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 mentioned this issue Mar 2, 2024
Closed
hendriktews added a commit to hendriktews/PG that referenced this issue Mar 3, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
c1dae22 
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 added a commit to hendriktews/PG that referenced this issue Mar 8, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
4e42494 
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 added a commit to hendriktews/PG that referenced this issue Apr 7, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
b984de6 
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 added a commit to hendriktews/PG that referenced this issue Apr 7, 2024
@hendriktews
coq: fix goals update after error
0b42f93 
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 added a commit to hendriktews/PG that referenced this issue Apr 17, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
0c8030d 
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 'coq-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
@hendriktews hendriktews mentioned this issue Apr 17, 2024
Open
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 18, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
e2c661d 
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 'coq-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
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 18, 2024
@hendriktews
clear goals buffer after Qed and Admitted when running silent
02a1007 
This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 21, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
6c392f1 
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 'coq-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
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 21, 2024
@hendriktews
clear goals buffer after Qed and Admitted when running silent
b7cb334 
This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 22, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
46134ee 
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 'coq-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
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 22, 2024
@hendriktews
clear goals buffer after Qed and Admitted when running silent
0758343 
This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 25, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
678f990 
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 'coq-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
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 25, 2024
@hendriktews
clear goals buffer after Qed and Admitted when running silent
140e076 
This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.
hendriktews added a commit to hendriktews/PG that referenced this issue May 12, 2024
@hendriktews
coq: run silently and explicitly Show when necessary
a218d44 
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
hendriktews added a commit to hendriktews/PG that referenced this issue May 12, 2024
@hendriktews
clear goals buffer after Qed and Admitted when running silent
b5b0255 
This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug kind: question kind: regression
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@Matafou @ejgallego @cpitclaudel @hendriktews