Fix NeoVim Deadlock (#361)

Calling :CoqJumpToEnd before :CoqStart results in a deadlock on NeoVim. The sequence of events is:
1. Since !s:running(), :CoqJumpToEndcalls coqtail#start with coqtail#jumpto("endpoint") as a callback.
2. coqtail#start calls s:call, which calls s:sendexpr and registers coqtail#after_startCB as its callback.
3. s:chanrecv receives the reply and executes coqtail#after_startCB.
4. coqtail#after_startCB executes coqtail#jumpto, which calls s:call, which calls s:evalexpr.
5. s:evalexpr blocks while waiting for a reply, but s:chanrecv is also blocked waiting for coqtail#after_startCB to return.

Commands like :CoqNext don't have this problem because they execute asynchronously, so coqtail#after_startCB calls s:sendexpr instead of s:evalexpr. It also works fine on Vim because it uses the builtin ch_evalexpr, which handles other messages while waiting for a reply.

The ideal solution would be to somehow execute callbacks asynchronously, but I couldn't figure out a way of doing that in vimscript. Perhaps it's possible with Lua. In any case, I realized that the only synchronous commands that could be called before :CoqStart are :CoqJumpToEnd, :CoqJumpToError, and :CoqGotoDef, so I just have these cases busy wait for coqtail#start to complete instead of using callbacks.

Fixes #360.

CHANGELOG.md

@@ -2,6 +2,10 @@
 
 ## Unreleased ([main])
 
+### Fixed
+- A deadlock in NeoVim when executing certain commands before `:CoqStart`.
+  (PR #361)
+
 ## [1.7.2]
 
 ### Added

autoload/coqtail.vim

@@ -340,18 +340,20 @@ function! coqtail#locate_dune() abort
   return l:file !=# ''
 endfunction
 
-" Launch Coqtop and open the auxiliary panels.
+" Launch Coqtop and open the auxiliary panels. `after_start_cmd` will be
+" executed by `coqtail#after_startCB` after Coqtop is started.
+" NOTE: It must not make a synchronous call or else NeoVim will deadlock. See
+" `s:chanrecv`.
 function! coqtail#start(after_start_cmd, coq_args) abort
   if s:running()
     call coqtail#util#warn('Coq is already running.')
   else
+    " See comment in coqtail#init() about buffer-local variables
     " Hack: buffer-local variable as we cannot easily pass this to
     " coqtail#after_startCB
     let b:after_start_cmd = a:after_start_cmd
 
-    " See comment in coqtail#init() about buffer-local variables
-    let b:coqtail_started = coqtail#init()
-    if !b:coqtail_started
+    if !coqtail#init()
       call coqtail#stop()
       return 0
     endif
@@ -360,7 +362,7 @@ function! coqtail#start(after_start_cmd, coq_args) abort
     call coqtail#panels#open(0)
 
     " Find Coqtop
-    let [l:ok, l:ver_or_msg] = s:call('find_coq', 'sync', 0, {
+    let [l:ok, l:ver_or_msg] = s:call('find_coq', 'sync', 1, {
       \ 'coq_path': expand(coqtail#util#getvar([b:, g:], 'coqtail_coq_path', $COQBIN)),
       \ 'coq_prog': coqtail#util#getvar([b:, g:], 'coqtail_coq_prog', '')})
     if !l:ok || type(l:ver_or_msg) == g:coqtail#compat#t_string
@@ -387,7 +389,7 @@ function! coqtail#start(after_start_cmd, coq_args) abort
 
     " Draw the logo
     let l:info_winid = bufwinid(b:coqtail_panel_bufs[g:coqtail#panels#info])
-    call s:call('splash', 'sync', 0, {
+    call s:call('splash', 'sync', 1, {
       \ 'version': b:coqtail_version.str_version,
       \ 'width': winwidth(l:info_winid),
       \ 'height': winheight(l:info_winid)})
@@ -427,7 +429,7 @@ function! coqtail#start(after_start_cmd, coq_args) abort
     let l:args = map(l:args_to_pass, 'expand(v:val)')
 
     " Launch Coqtop asynchronously
-    call s:call('start', 'coqtail#after_startCB', 0, {
+    call s:call('start', 'coqtail#after_startCB', 1, {
       \ 'coqproject_args': l:args,
       \ 'use_dune': coqtail#util#getvar([b:], 'coqtail_use_dune', 0),
       \ 'dune_compile_deps': coqtail#util#getvar([b:, g:], 'coqtail_dune_compile_deps', 0)})
@@ -472,6 +474,7 @@ function! coqtail#after_startCB(chan, msg) abort
 
   call s:init_proof_diffs(b:coqtail_version.str_version)
 
+  let b:coqtail_started = 1
   " Call the after_start_cmd, if present
   if b:after_start_cmd != v:null
     execute b:after_start_cmd
@@ -482,7 +485,6 @@ function! coqtail#after_startCB(chan, msg) abort
   execute g:coqtail#util#bufchangepre 'buffer' l:buf
 endfunction
 
-
 " Stop the Coqtop interface and clean up auxiliary panels.
 function! coqtail#stop() abort
   " Set a 'coqtail_stopping' flag in order to prevent multiple stop signals or
@@ -580,11 +582,26 @@ let s:cmd_opts = {
 \}
 
 function! s:cmddef(name, act, precmd) abort
-  " Start Coqtail first if needed
+  " '': Don't wait.
+  " 's' (start): Wait for everything to fully start (Coqtail server, Coqtop
+  "              server, Goal and Info panels, etc) by registering the command
+  "              as a callback to `coqtail#start`.
+  " 'i' (initialize): Wait for the Coqtail server to start. Only used for
+  "                   `CoqToggleDebug`.
+  " 'b' (busy-wait): Wait for everything to fully start by sleeping until
+  "                  `coqtail#start` completes. Only used for `CoqJumpToEnd`,
+  "                  `CoqJumpToError`, and `CoqGotoDef`. This avoids a deadlock
+  "                  in NeoVim from calling synchronous commands from callbacks.
   let l:act = {
     \ '_': a:act,
-    \ 's': printf('if s:running() | %s | else | call coqtail#start(%s, []) | endif', a:act, string(a:act)),
-    \ 'i': printf('if s:initted() || coqtail#init() | %s | endif', a:act)
+    \ 's': printf(
+      \ 'if s:running() | %s | else | call coqtail#start(%s, []) | endif',
+      \ a:act,
+      \ string(a:act)),
+    \ 'i': printf('if s:initted() || coqtail#init() | %s | endif', a:act),
+    \ 'b': printf(
+      \ 'if !s:running() | call coqtail#start(v:null, []) | endif | while !s:running() | sleep 10m | endwhile | %s',
+      \ a:act)
   \}[a:precmd ==# '' ? '_' : a:precmd]
   execute printf('command! -buffer %s %s %s', s:cmd_opts[a:name], a:name, l:act)
 endfunction
@@ -599,9 +616,9 @@ function! coqtail#define_commands() abort
   call s:cmddef('CoqToLine', 'call coqtail#toline(<count>, 0)', 's')
   call s:cmddef('CoqOmitToLine', 'call coqtail#toline(<count>, 1)', 's')
   call s:cmddef('CoqToTop', 'call s:call("to_top", "", 0, {})', 's')
-  call s:cmddef('CoqJumpToEnd', 'call coqtail#jumpto("endpoint")', 's')
-  call s:cmddef('CoqJumpToError', 'call coqtail#jumpto("errorpoint")', 's')
-  call s:cmddef('CoqGotoDef', 'call coqtail#gotodef(<f-args>, <bang>0)', 's')
+  call s:cmddef('CoqJumpToEnd', 'call coqtail#jumpto("endpoint")', 'b')
+  call s:cmddef('CoqJumpToError', 'call coqtail#jumpto("errorpoint")', 'b')
+  call s:cmddef('CoqGotoDef', 'call coqtail#gotodef(<f-args>, <bang>0)', 'b')
   call s:cmddef('Coq', 'call s:call("query", "", 0, {"args": [<f-args>]})', 's')
   call s:cmddef('CoqRestorePanels',
     \ 'call coqtail#panels#open(1) | call coqtail#refresh()', 's')

autoload/coqtail/channel.vim

@@ -116,6 +116,8 @@ elseif g:coqtail#compat#nvim
         if has_key(s:replies, l:msg_id)
           let s:replies[l:msg_id] = l:data
         elseif has_key(s:callbacks, l:msg_id)
+          " This will deadlock if the callback calls `s:evalexpr` since
+          " `s:chanrecv` can only handle one message at a time.
           call call(s:callbacks[l:msg_id], [a:handle, l:data])
           unlet s:callbacks[l:msg_id]
         endif

python/coqtail.py

@@ -827,10 +827,8 @@ def toggle_debug(self, opts: VimOptions) -> None:
         log = self.coqtop.toggle_debug()
         if log is None:
             msg = "Debugging disabled."
-            self.log = ""
         else:
             msg = f"Debugging enabled. Log: {log}."
-            self.log = log
 
         self.set_info(msg, reset=True)
         self.refresh(goals=False, opts=opts)

python/coqtop.py

@@ -112,7 +112,6 @@ def __init__(
         self.logger = logging.getLogger(str(id(self)))
         self.logger.addHandler(self.handler)
         self.logger.setLevel(logging.INFO)
-        self.toggle_debug()
 
     def is_in_valid_dune_project(self, filename: str) -> bool:
         """Query dune to assert that the given file is in a correctly configured dune project."""

python/xmlInterface.py

@@ -798,9 +798,9 @@ def __init__(
                 "goal": self._to_goal,
                 "goals": self._to_goals,
                 "evar": self._to_evar,
-                "option_value": self._to_option_value,
+                "option_value": self._to_option_value,  # type: ignore
                 "option_state": self._to_option_state,
-                "status": self._to_status,
+                "status": self._to_status,  # type: ignore
                 "coq_info": self._to_coq_info,
                 "message": self._to_message,
                 "feedback": self._to_feedback,
@@ -1156,10 +1156,10 @@ def __init__(
                 "goal": self._to_goal,
                 "goals": self._to_goals,
                 "evar": self._to_evar,
-                "option_value": self._to_option_value,
+                "option_value": self._to_option_value,  # type: ignore
                 "option_state": self._to_option_state,
                 "state_id": self._to_state_id,
-                "status": self._to_status,
+                "status": self._to_status,  # type: ignore
                 "coq_info": self._to_coq_info,
                 "message": self._to_message,
                 "feedback": self._to_feedback,