diff --git a/CHANGELOG.md b/CHANGELOG.md index 7f8100da..d99041b0 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/python/xmlInterface.py b/python/xmlInterface.py index 093edab4..13ff9982 100644 --- a/python/xmlInterface.py +++ b/python/xmlInterface.py @@ -1891,10 +1891,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: + + """ + + 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: + val | + state_id (option loc) msg + """ + # 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), @@ -1912,6 +1981,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] diff --git a/tests/coq/test_coqtop.py b/tests/coq/test_coqtop.py index e6bdfe4c..d2d759ce 100644 --- a/tests/coq/test_coqtop.py +++ b/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."""