Skip to content

Commit

Permalink
Avoid race condition while starting coqtail
Browse files Browse the repository at this point in the history
As described in #364, now that `coqtail#start` calls `start` asynchronously,
calling a command during `CoqStart` (e.g., `:CoqToLine | CoqToLine`) can cause
a race that often results in a fatal error. The solution implemented here is to
have `coqtail#start` check if Coqtail is initialized (`s:initted()`) but not
yet running (`s:running()`) and, if so, drop the command with a warning. The
only difference between `s:initted()` and `s:running()` is whether
`b:coqtail_started` is set, so I believe this should ensure that no other
commands can run until `coqtail#after_startCB` completes. Since I expect it
should be pretty rare in practice for someone to try to run commands before
`CoqStart` completes, I think just ignoring them is reasonable. This should not
affect commands that are called before `CoqStart`, those will still be queued
to run by `coqtail#after_startCB`.

Fixes #364.
  • Loading branch information
whonore committed Aug 23, 2024
1 parent 7e37111 commit b50e57b
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions autoload/coqtail.vim
Original file line number Diff line number Diff line change
Expand Up @@ -347,6 +347,8 @@ endfunction
function! coqtail#start(after_start_cmd, coq_args) abort
if s:running()
call coqtail#util#warn('Coq is already running.')
elseif s:initted()
call coqtail#util#warn('Coq is still starting.')
else
" See comment in coqtail#init() about buffer-local variables
" Hack: buffer-local variable as we cannot easily pass this to
Expand Down

0 comments on commit b50e57b

Please sign in to comment.