From e52c456d44e2e3c580428e54182a59d82009c3e2 Mon Sep 17 00:00:00 2001
From: Jade Sailor <jsailor-github@jesnetplus.com>
Date: Sat, 17 Feb 2024 08:44:03 -0500
Subject: [PATCH] Fix goals panel when no proof is active on Coq >= 8.16.
 (#337)

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.
---
 CHANGELOG.md     |  4 ++++
 python/coqtop.py | 28 +++++++++++++++++-----------
 2 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3b9d0a80..1a91f7e9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,10 @@
 
 ## Unreleased ([main])
 
+### Fixed
+- Fix rendering of goals panel when no proof is active in Coq >= 8.16.
+  (PR #337)
+
 ## [1.7.1]
 
 ### Added
diff --git a/python/coqtop.py b/python/coqtop.py
index dee59718..795e42b1 100644
--- a/python/coqtop.py
+++ b/python/coqtop.py
@@ -318,7 +318,8 @@ def subgoals(
         """Get the current set of hypotheses and goals."""
         assert self.xml is not None
 
-        # Get only the focused goals
+        # Get the current proof state, but only include focused
+        # goals in the goal list.
         response_main, err_main = self.call(
             self.xml.subgoal(  # type: ignore
                 GoalMode.FULL,
@@ -333,6 +334,13 @@ def subgoals(
         if isinstance(response_main, Err):
             return (False, response_main.msg, None, err_main)
 
+        # If success but we didn't get a CoqGoals, then there's
+        # no proof in progress. We can return early.
+        if response_main.val is None:
+            # If the request was success but it returned None, then
+            # we're not in a proof. No need to run the second query.
+            return (True, response_main.msg, None, err_main)
+
         # NOTE: Subgoals ignores `gf_flag = "short"` if proof diffs are
         # enabled.
         # See: https://github.com/coq/coq/issues/16564
@@ -356,19 +364,17 @@ def subgoals(
         if isinstance(response_extra, Err):
             return (False, msgs, None, errs)
 
+        assert response_extra.val is not None, "proof state changed unexpectedly?"
+
         # Merge goals
-        fg = response_main.val.fg if response_main.val is not None else []
-        bg, shelved, given_up = (
-            (
-                response_extra.val.bg,
-                response_extra.val.shelved,
-                response_extra.val.given_up,
-            )
-            if response_extra.val is not None
-            else ([], [], [])
+        goals = Goals(
+            response_main.val.fg,
+            response_extra.val.bg,
+            response_extra.val.shelved,
+            response_extra.val.given_up,
         )
 
-        return (True, msgs, Goals(fg, bg, shelved, given_up), errs)
+        return (True, msgs, goals, errs)
 
     def do_option(
         self,