From 7f4c5feaf0f01e8991ebb9b12d4fb98216caadb0 Mon Sep 17 00:00:00 2001
From: whonore <wolfhonore@gmail.com>
Date: Tue, 17 Sep 2024 08:58:16 -0700
Subject: [PATCH] Condition unprintable test on Coq version

---
 tests/coq/test_coqtop.py | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/tests/coq/test_coqtop.py b/tests/coq/test_coqtop.py
index 0b28130a..c49285d7 100644
--- a/tests/coq/test_coqtop.py
+++ b/tests/coq/test_coqtop.py
@@ -135,14 +135,23 @@ def test_dispatch_unicode(coq: Coqtop) -> None:
 
 def test_dispatch_unprintable(coq: Coqtop) -> None:
     """Should be able to handle unprintable characters."""
-    succ, _, _, _ = coq.dispatch("Definition parse (x : Byte.byte) : option nat := None.")
-    assert succ
-    succ, _, _, _ = coq.dispatch("Definition print (x : nat) : list Byte.byte := cons Byte.x00 nil.")
-    assert succ
-    succ, _, _, _ = coq.dispatch("String Notation nat parse print : nat_scope.")
-    assert succ
-    succ, out, _, _ = coq.dispatch("Check O.")
-    assert succ
+    assert coq.xml is not None
+    cmds = (
+        [
+            "Definition parse (x : Byte.byte) : option nat := None.",
+            "Definition print (x : nat) : list Byte.byte := cons Byte.x00 nil.",
+            "String Notation nat parse print : nat_scope.",
+            "Check O.",
+        ]
+        if coq.xml.version >= (8, 20, 0)
+        else [
+            "Require Import String.",
+            "Compute String (Ascii.ascii_of_nat 0) EmptyString.",
+        ]
+    )
+    for cmd in cmds:
+        succ, out, _, _ = coq.dispatch(cmd)
+        assert succ
     assert "\\x00" in out