Add g:coqtail_treat_stderr_as_warning (#338)

CHANGELOG.md

@@ -2,6 +2,10 @@
 
 ## Unreleased ([main])
 
+### Added
+- `g:coqtail_treat_stderr_as_warning` option to ignore unrecognized warnings on stderr.
+  (PR #338)
+
 ### Fixed
 - Fix rendering of goals panel when no proof is active in Coq >= 8.16.
   (PR #337)

autoload/coqtail.vim

@@ -39,6 +39,11 @@ if !exists('g:coqtail_update_tagstack')
   let g:coqtail_update_tagstack = 1
 endif
 
+" Default to not treating all stderr messages as warnings.
+if !exists('g:coqtail_treat_stderr_as_warning')
+  let g:coqtail_treat_stderr_as_warning = 0
+endif
+
 " Find the path corresponding to 'lib'. Used by includeexpr.
 function! coqtail#findlib(lib) abort
   let [l:ok, l:lib] = s:call('find_lib', 'sync', 0, {'lib': a:lib})
@@ -224,7 +229,8 @@ function! s:call(cmd, cb, nocoq, args) abort
   let a:args.opts = {
     \ 'encoding': &encoding,
     \ 'timeout': coqtail#panels#getvar('coqtail_timeout'),
-    \ 'filename': expand('#' . b:coqtail_panel_bufs.main . ':p')
+    \ 'filename': expand('#' . b:coqtail_panel_bufs.main . ':p'),
+    \ 'stderr_is_warning': g:coqtail_treat_stderr_as_warning
   \}
   let l:args = [b:coqtail_panel_bufs.main, a:cmd, a:args]
 

doc/coqtail.txt

@@ -359,6 +359,20 @@ g:coqtail_tagfunc	If true then set 'tagfunc' to `coqtail#gettags`.
 
 			Default: 1
 
+					     *g:coqtail_treat_stderr_as_warning*
+					       *coqtail-treat-stderr-as-warning*
+g:coqtail_treat_stderr_as_warning
+			If true then assume all messages received from Coq on
+			stderr are only warnings. Warnings are reported in the
+			Info panel, but do not prevent checking subsequent
+			sentences. This shouldn't be necessary in most cases
+			as Coqtail can automatically recognize warning
+			messages that follow a standard format, and generally,
+			messages should be sent via the XML protocol rather
+			than stderr.
+
+			Default: 0
+
 =======================
 Backwards Compatibility			       *coqtail-backwards-compatibility*
 

python/coqtail.py

@@ -58,7 +58,12 @@
     ResQueue = Queue[Res]
     VimOptions = TypedDict(
         "VimOptions",
-        {"encoding": str, "timeout": int, "filename": str},
+        {
+            "encoding": str,
+            "timeout": int,
+            "filename": str,
+            "stderr_is_warning": bool,
+        },
     )
     ResFuture = futures.Future[Optional[str]]
 else:
@@ -203,6 +208,7 @@ def start(
                 opts["filename"],
                 args,
                 timeout=opts["timeout"],
+                stderr_is_warning=opts["stderr_is_warning"],
             )
             self.print_stderr(stderr)
         except (ValueError, CT.CoqtopError) as e:
@@ -253,7 +259,10 @@ def rewind(self, steps: int, opts: VimOptions) -> Optional[str]:
             return None
 
         try:
-            _, msg, extra_steps, stderr = self.coqtop.rewind(steps)
+            _, msg, extra_steps, stderr = self.coqtop.rewind(
+                steps,
+                stderr_is_warning=opts["stderr_is_warning"],
+            )
             self.print_stderr(stderr)
         except CT.CoqtopError as e:
             return str(e)
@@ -405,6 +414,7 @@ def send_until_fail(
                     no_comments.decode("utf-8"),
                     encoding=opts["encoding"],
                     timeout=opts["timeout"],
+                    stderr_is_warning=opts["stderr_is_warning"],
                 )
             except CT.CoqtopError as e:
                 return None, str(e)
@@ -460,6 +470,7 @@ def do_query(self, query: str, opts: VimOptions) -> Tuple[bool, str, str]:
                 in_script=False,
                 encoding=opts["encoding"],
                 timeout=opts["timeout"],
+                stderr_is_warning=opts["stderr_is_warning"],
             )
         except CT.CoqtopError as e:
             return False, str(e), ""
@@ -581,7 +592,10 @@ def refresh(
     def get_goals(self, opts: VimOptions) -> Tuple[Optional[Goals], str]:
         """Get the current goals."""
         try:
-            _, msg, goals, stderr = self.coqtop.goals(timeout=opts["timeout"])
+            _, msg, goals, stderr = self.coqtop.goals(
+                timeout=opts["timeout"],
+                stderr_is_warning=opts["stderr_is_warning"],
+            )
             self.print_stderr(stderr)
             return goals, msg
         except CT.CoqtopError as e: