Support Subgoals command (whonore#309)

Fix whonore#55

CHANGELOG.md

@@ -2,6 +2,12 @@
 
 ## Unreleased ([master])
 
+### Added
+- Support for the `Subgoals` XML command (>= 8.16 only).
+  This should speed up displaying the current goal when there are many
+  unfocused/shelved/admitted goals with large proof contexts.
+  (PR #309)
+
 ### Fixed
 - Joining comments with `J` while the `j` flag is set in `'formatoptions'` does
   not delete the second line.

python/coqtop.py

@@ -9,12 +9,14 @@
 import threading
 import time
 from concurrent import futures
+from contextlib import contextmanager
 from queue import Empty, Queue
 from tempfile import NamedTemporaryFile
 from typing import (
     IO,
     TYPE_CHECKING,
     Any,
+    Generator,
     Iterable,
     Iterator,
     List,
@@ -29,6 +31,7 @@
     UNEXPECTED_ERR,
     Err,
     FindCoqtopError,
+    GoalMode,
     Goals,
     Ok,
     Result,
@@ -57,6 +60,11 @@
     VersionInfo = Mapping[str, Any]
 
 
+def join_not_empty(msgs: Iterable[str], joiner: str = "\n\n") -> str:
+    """Concatenate non-empty messages."""
+    return joiner.join(msg for msg in msgs if msg != "")
+
+
 class CoqtopError(Exception):
     """An exception for when Coqtop stops unexpectedly."""
 
@@ -209,11 +217,7 @@ def advance(
         status, err2 = self.call(self.xml.status(encoding=encoding), timeout=timeout)
 
         # Combine messages
-        msgs = "\n\n".join(
-            msg
-            for msg in (response.msg, response.val["res_msg"], status.msg)
-            if msg != ""
-        )
+        msgs = join_not_empty((response.msg, response.val["res_msg"], status.msg))
         err = err1 + err2
 
         if isinstance(status, Err):
@@ -293,6 +297,11 @@ def goals(
         """Get the current set of hypotheses and goals."""
         assert self.xml is not None
         self.logger.debug("goals")
+
+        # Use Subgoals if available, otherwise fall back to Goal
+        if hasattr(self.xml, "subgoal"):
+            return self.subgoals(timeout=timeout)
+
         response, err = self.call(self.xml.goal(), timeout=timeout)
 
         return (
@@ -302,6 +311,65 @@ def goals(
             err,
         )
 
+    def subgoals(
+        self,
+        timeout: Optional[int] = None,
+    ) -> Tuple[bool, str, Optional[Goals], str]:
+        """Get the current set of hypotheses and goals."""
+        assert self.xml is not None
+
+        # Get only the focused goals
+        response_main, err_main = self.call(
+            self.xml.subgoal(  # type: ignore
+                GoalMode.FULL,
+                fg=True,
+                bg=False,
+                shelved=False,
+                given_up=False,
+            ),
+            timeout=timeout,
+        )
+
+        if isinstance(response_main, Err):
+            return (False, 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
+        with self.suppress_diffs():
+            # Get the short version of other goals (no hypotheses)
+            response_extra, err_extra = self.call(
+                self.xml.subgoal(  # type: ignore
+                    GoalMode.SHORT,
+                    fg=False,
+                    bg=True,
+                    shelved=True,
+                    given_up=True,
+                ),
+                timeout=timeout,
+            )
+
+        # Combine messages
+        msgs = join_not_empty(response_main.msg, response_extra.msg)
+        errs = err_main + err_extra
+
+        if isinstance(response_extra, Err):
+            return (False, msgs, None, errs)
+
+        # 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 ([], [], [])
+        )
+
+        return (True, msgs, Goals(fg, bg, shelved, given_up), errs)
+
     def do_option(
         self,
         cmd: str,
@@ -381,6 +449,50 @@ def dispatch(
         else:
             return True, "Command only allowed in script.", None, ""
 
+    @contextmanager
+    def suppress_diffs(
+        self,
+        timeout: Optional[int] = None,
+    ) -> Generator[None, None, None]:
+        """Temporarily disable proof diffs."""
+        # Check if diffs are enabled
+        expect_prefix = "Diffs: Some(val="
+        ok, response, _, err = self.do_option(
+            "Test Diffs",
+            in_script=False,
+            timeout=timeout,
+        )
+        if ok and response.startswith(expect_prefix):
+            # TODO: Make a cleaner way of reading an option
+            diffs = response[len(expect_prefix) : -1].strip("'")
+        else:
+            # Failures are just logged because there's not much else that can
+            # be done from here.
+            self.logger.warning("Failed to read Diffs option: %s", err)
+            diffs = "off"
+
+        # Disable if necessary
+        if diffs != "off":
+            ok, _, _, err = self.do_option(
+                'Set Diffs "off"',
+                in_script=False,
+                timeout=timeout,
+            )
+            if not ok:
+                self.logger.warning("Failed to disable Diffs option: %s", err)
+
+        yield None
+
+        # Re-enable if necessary
+        if diffs != "off":
+            ok, _, _, err = self.do_option(
+                f'Set Diffs "{diffs}"',
+                in_script=False,
+                timeout=timeout,
+            )
+            if not ok:
+                self.logger.warning("Failed to re-enable Diffs option: %s", err)
+
     # Interacting with Coqtop #
     def call(
         self,

python/xmlInterface.py

@@ -11,6 +11,7 @@
 import subprocess
 import xml.etree.ElementTree as ET
 from abc import ABCMeta, abstractmethod
+from enum import Enum
 from pathlib import Path
 from shutil import which
 from typing import (
@@ -50,6 +51,16 @@
     ],
 )
 
+
+class GoalMode(Enum):
+    """Control the information returned by the Subgoals command."""
+
+    # Get the goal and hypotheses
+    FULL = "full"
+    # Get only the goal
+    SHORT = "short"
+
+
 WARNING_RE = re.compile("^(Warning:[^]]+])$", flags=re.MULTILINE)
 
 
@@ -1794,6 +1805,60 @@ def _standardize_add(self, res: Result) -> Result:
 class XMLInterface816(XMLInterface815):
     """The version 8.16.* XML interface."""
 
+    CoqGoalFlags = NamedTuple(
+        "CoqGoalFlags",
+        [
+            ("mode", str),
+            ("fg", bool),
+            ("bg", bool),
+            ("shelved", bool),
+            ("given_up", bool),
+        ],
+    )
+
+    def __init__(
+        self,
+        version: Tuple[int, int, int],
+        str_version: str,
+        coq_path: str,
+        coq_prog: Optional[str],
+    ) -> None:
+        """Update conversion maps with new types."""
+        super().__init__(version, str_version, coq_path, coq_prog)
+
+        self._of_py_funcs.update({"CoqGoalFlags": self._of_goal_flags})
+
+        self._standardize_funcs.update({"Subgoals": self._standardize_goal})
+
+    def _of_goal_flags(self, val: CoqGoalFlags) -> ET.Element:
+        """Expect: CoqGoalFlags(str, bool, bool, bool, bool)"""
+        return self._build_xml(
+            "goal_flags",
+            children=[val.mode, val.fg, val.bg, val.shelved, val.given_up],
+        )
+
+    def subgoal(
+        self,
+        mode: GoalMode,
+        fg: bool = True,
+        bg: bool = True,
+        shelved: bool = True,
+        given_up: bool = True,
+        encoding: str = "utf-8",
+    ) -> Tuple[str, Optional[bytes]]:
+        """Create an XML string to check the state a specific set of goals.
+        Args:
+          flags: CoqGoalFlags - Which goals to return
+        """
+        return (
+            "Subgoals",
+            self._make_call(
+                encoding,
+                "Subgoals",
+                children=self.CoqGoalFlags(mode.value, fg, bg, shelved, given_up),
+            ),
+        )
+
 
 XMLInterfaces = (
     ((8, 4, 0), (8, 5, 0), XMLInterface84),