Skip warning messages when running vernacular queries

src/coq_serapy/serapi_backend.py

@@ -17,7 +17,7 @@
                           NoSuchGoalError)
 from .contexts import ProofContext, Obligation, SexpObligation
 from .coq_util import raise_, parsePPSubgoal, setup_opam_env, get_module_from_filename
-from .util import (eprint, parseSexpOneLevel, unwrap, progn)
+from .util import (eprint, parseSexpOneLevel, unwrap, progn, kill_process_and_children)
 if TYPE_CHECKING:
     from sexpdata import Sexp
 
@@ -168,8 +168,9 @@ def getProofContext(self) -> Optional[ProofContext]:
 
     def close(self) -> None:
         assert self._proc.stdout
-        self._proc.terminate()
-        self._proc.kill()
+        kill_process_and_children(self._proc)
+        # self._proc.terminate()
+        # self._proc.kill()
         self.__sema.release()
     def isInProof(self) -> bool:
         return self.proof_context is not None
@@ -297,7 +298,7 @@ def get_all_sexp_goals(self) -> List[SexpObligation]:
             return []
     def _isFeedbackMessage(self, msg: str) -> bool:
         # if self.coq_minor_version() > 12:
-        return isFeedbackMessage(msg)
+        return isFeedbackMessage(msg) or isFeedbackWarningMessage(msg) or isFeedbackMessageOld(msg)
         # return isFeedbackMessageOld(msg)
     def _flush_queue(self) -> None:
         while not self.message_queue.empty():
@@ -770,6 +771,15 @@ def isFeedbackMessage(msg: 'Sexp') -> bool:
                  lambda *args: True,
                  _, lambda *args: False)
 
+def isFeedbackWarningMessage(msg: 'Sexp') -> bool:
+    return match(normalizeMessage(msg, depth=6),
+                 ["Feedback", [["doc_id", int], ["span_id", int],
+                               ["route", int],
+                               ["contents", ["Message", ["level", "Warning"],
+                                             ["loc", []], TAIL]]]],
+                 lambda *args: True,
+                 _, lambda *args: False)
+
 def isProgressMessage(msg: 'Sexp') -> bool:
     return match(normalizeMessage(msg),
                  ["Feedback", [["doc_id", int], ["span_id", int],

src/coq_serapy/util.py

@@ -6,11 +6,18 @@
 import sys
 
 from typing import (Optional, Tuple, TypeVar, Union, List, Pattern, Match)
+import subprocess
+import psutil
 
 from sexpdata import Symbol
 
 T = TypeVar('T')
 
+def kill_process_and_children(process: subprocess.Popen):
+    for child in psutil.Process(process.pid).children(recursive=True):
+        child.kill()
+    process.kill()
+
 
 def unwrap(a: Optional[T]) -> T:
     assert a is not None