Adapt to new error location type (#358)

coq/coq#19040 changes the way error locations are
reported in the XML protocol. Specifically, it replaces the `loc_s` and `loc_e`
attributes of the `fail` result with an optional `Loc.t` field. If I understand
correctly, the `start` and `stop` fields contain the same byte offsets as the
old `loc_s` and `loc_e`, so it's enough to just extract and return those.

CHANGELOG.md

@@ -3,6 +3,9 @@
 ## Unreleased ([main])
 
 ### Added
+- Preliminary support for Coq 8.20 by adapting to the new type used to report
+  error locations.
+  (PR #358)
 - `g:coqtail_treat_stderr_as_warning` option to ignore unrecognized warnings on stderr.
   (PR #338)
 - Add a hook for more flexible keybindings.

python/xmlInterface.py

@@ -1890,10 +1890,79 @@ class XMLInterface818(XMLInterface817):
     """The version 8.18.* XML interface."""
 
 
-class XMLInterface819(XMLInterface817):
+class XMLInterface819(XMLInterface818):
     """The version 8.19.* XML interface."""
 
 
+class XMLInterface820(XMLInterface819):
+    """The version 8.20.* XML interface."""
+
+    Loc = NamedTuple(
+        "Loc",
+        [
+            ("start", int),
+            ("stop", int),
+            ("line_nb", int),
+            ("bol_pos", int),
+            ("line_nb_last", int),
+            ("bol_pos_last", int),
+        ],
+    )
+
+    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._to_py_funcs.update({"loc": self._to_loc})
+
+    def _to_loc(self, xml: ET.Element) -> Loc:
+        """Expect:
+        <loc start="int" stop="int" line_nb="int" bol_pos="int"
+             line_nb_last="int" bol_pos_last="int" />
+        """
+
+        def assert_int(v: Optional[str]) -> int:
+            assert v is not None
+            return int(v)
+
+        return self.Loc(
+            assert_int(xml.get("start")),
+            assert_int(xml.get("stop")),
+            assert_int(xml.get("line_nb")),
+            assert_int(xml.get("bol_pos")),
+            assert_int(xml.get("line_nb_last")),
+            assert_int(xml.get("bol_pos_last")),
+        )
+
+    # Overrides _to_response from XMLInterfaceBase
+    def _to_response(self, xml: ET.Element) -> Result:
+        """Expect:
+        <value val="good">val</value> |
+        <value val="fail">state_id (option loc) msg</value>
+        """
+        # pylint: disable=no-else-return
+        val = xml.get("val")
+
+        if val == "good":
+            return Ok(self._to_py(xml[0]))
+        elif val == "fail":
+            loc = self._to_py(xml[1])
+            loc_s, loc_e = (
+                (loc.val.start, loc.val.stop) if loc is not None else (-1, -1)
+            )
+
+            msg = "".join(xml.itertext())
+
+            return Err(msg, (loc_s, loc_e))
+        raise unexpected(("good", "fail"), val)
+
+
 XMLInterfaces = (
     ((8, 4, 0), (8, 5, 0), XMLInterface84),
     ((8, 5, 0), (8, 6, 0), XMLInterface85),
@@ -1911,6 +1980,7 @@ class XMLInterface819(XMLInterface817):
     ((8, 17, 0), (8, 18, 0), XMLInterface817),
     ((8, 18, 0), (8, 19, 0), XMLInterface818),
     ((8, 19, 0), (8, 20, 0), XMLInterface819),
+    ((8, 20, 0), (8, 21, 0), XMLInterface820),
 )
 
 XMLInterfaceLatest = XMLInterfaces[-1][2]

tests/coq/test_coqtop.py

@@ -168,17 +168,35 @@ def test_goals_no_change(coq: Coqtop) -> None:
 def test_advance_fail(coq: Coqtop) -> None:
     """If advance fails then the state will not change."""
     old_state = get_state(coq)
-    fail, _, _, _ = coq.dispatch("SyntaxError")
-    assert not fail
+    succ, _, _, _ = coq.dispatch("SyntaxError.")
+    assert not succ
     assert old_state == get_state(coq)
     succ, _, _, _ = coq.dispatch("Lemma x : False.")
     assert succ
     old_state = get_state(coq)
-    fail, _, _, _ = coq.dispatch("reflexivity.")
-    assert not fail
+    succ, _, _, _ = coq.dispatch("reflexivity.")
+    assert not succ
     assert old_state == get_state(coq)
 
 
+def test_advance_fail_err_loc(coq: Coqtop) -> None:
+    """If advance fails then the error locations are correct."""
+    assert coq.xml is not None
+    succ, _, err_loc, _ = coq.dispatch("SyntaxError.")
+    assert not succ
+    assert err_loc is not None
+    if coq.xml.version < (8, 5, 0):
+        assert err_loc == (-1, -1)
+    elif (8, 5, 0) <= coq.xml.version < (8, 6, 0):
+        assert err_loc == (0, 12)
+    else:
+        assert err_loc == (0, 11)
+    succ, _, err_loc, _ = coq.dispatch("Definition α := not_defined.")
+    assert not succ
+    assert err_loc is not None
+    assert err_loc == (17, 28)
+
+
 # TODO: move interrupt tests to a separate file
 # def test_advance_stop(coq: Coqtop) -> None:
 #     """If advance is interrupted then the state will not change."""