Fix goals panel when no proof is active on Coq >= 8.16. #337
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
Traditionally, Coq IDEs used the 'Goals' XML command to get the proof state, which had the downside that the full details of non-foreground goals would get serialized from coqidetop but never displayed. In Coq 8.16, the 'Subgoals' command was added, which allows more precise goal fetching: IDEs can make one Subgoals call to request the focused goal in full detail, and another call to request just the conclusions of the other goals. Coqtail switched to this pattern in v1.7.1. Unfortunately, the logic for merging results from the two calls was slightly wrong. If the calls return None, then there is no proof in progress, but the logic in Coqtail handled this as if there is an in-progress proof with no remaining goals. This made the Goals panel always show "0 subgoals" even when no proof was in progress. Fix it. If the first call returns None, there is no proof in progress, and we don't bother to make the second call. Else, we learned that there is a proof in progress and what the foreground goal (if any) is; we make the second call to learn the other goals, and then merge the results and continue as before. Fixes c077a72.
|
Thanks for the fix, this looks great. |
|
@whonore Thanks! I appreciate the style fix; I didn't have a full python dev env handy to see them locally. |
Rixxc
pushed a commit
to Rixxc/Coqtail
that referenced
this pull request
Jul 2, 2024
Traditionally, Coq IDEs used the 'Goals' XML command to get the proof state, which had the downside that the full details of non-foreground goals would get serialized from coqidetop but never displayed. In Coq 8.16, the 'Subgoals' command was added, which allows more precise goal fetching: IDEs can make one Subgoals call to request the focused goal in full detail, and another call to request just the conclusions of the other goals. Coqtail switched to this pattern in v1.7.1. Unfortunately, the logic for merging results from the two calls was slightly wrong. If the calls return None, then there is no proof in progress, but the logic in Coqtail handled this as if there is an in-progress proof with no remaining goals. This made the Goals panel always show "0 subgoals" even when no proof was in progress. Fix it. If the first call returns None, there is no proof in progress, and we don't bother to make the second call. Else, we learned that there is a proof in progress and what the foreground goal (if any) is; we make the second call to learn the other goals, and then merge the results and continue as before. Fixes c077a72.
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.
Traditionally, Coq IDEs used the 'Goals' XML command to get the proof state, which had the downside that the full details of non-foreground goals would get serialized from coqidetop but never displayed. In Coq 8.16, the 'Subgoals' command was added, which allows more precise goal fetching: IDEs can make one Subgoals call to request the focused goal in full detail, and another call to request just the conclusions of the other goals. Coqtail switched to this pattern in v1.7.1.
Unfortunately, the logic for merging results from the two calls was slightly wrong. If the calls return None, then there is no proof in progress, but the logic in Coqtail handled this as if there is an in-progress proof with no remaining goals. This made the Goals panel always show "0 subgoals" even when no proof was in progress.
Fix it. If the first call returns None, there is no proof in progress, and we don't bother to make the second call. Else, we learned that there is a proof in progress and what the foreground goal (if any) is; we make the second call to learn the other goals, and then merge the results and continue as before.
Fixes c077a72.