whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 35 forks source link

Fix goals panel when no proof is active on Coq >= 8.16. #337

Closed jesboat closed 8 months ago

jesboat commented 8 months ago

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 c077a72329dc30fa22802a3a7de49856cb0f1fca.

whonore commented 8 months ago

Thanks for the fix, this looks great.

jesboat commented 8 months ago

@whonore Thanks! I appreciate the style fix; I didn't have a full python dev env handy to see them locally.