Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

race between coqtail#start and CoqToLine #364

Closed
tomtomjhj opened this issue Aug 9, 2024 · 2 comments · Fixed by #366
Closed

race between coqtail#start and CoqToLine #364

tomtomjhj opened this issue Aug 9, 2024 · 2 comments · Fixed by #366

Comments

@tomtomjhj
Copy link
Contributor

After ac6e91f, in both vim (9.1) and neovim (0.11-dev), I get the following error when I run :CoqToLine while coqtail is initializing.

Error detected while processing function coqtail#start[18]..<SNR>41_call[27]..<SNR>48_evalexpr:
line    1:
----------------------------------------
Exception occurred during processing of request from ('127.0.0.1', 45512)
Traceback (most recent call last):
  File "/usr/lib/python3.10/socketserver.py", line 683, in process_request_thread
    self.finish_request(request, client_address)
  File "/usr/lib/python3.10/socketserver.py", line 360, in finish_request
    self.RequestHandlerClass(request, client_address, self)
  File "/usr/lib/python3.10/socketserver.py", line 747, in __init__
    self.handle()
  File "/home/user/.vim/plugged/Coqtail/python/coqtail.py", line 969, in handle
    ret = handler(**args) if handler is not None else None
  File "/home/user/.vim/plugged/Coqtail/python/coqtail.py", line 205, in find_coq
    ver_or_err = self.coqtop.find_coq(
  File "/home/user/.vim/plugged/Coqtail/python/coqtop.py", line 222, in find_coq
    assert self.coqtop is None
AssertionError
----------------------------------------
Error detected while processing function coqtail#start:
line   18:
E714: List required

This can be consistently reproduced by running :CoqToLine|CoqToLine on a coq buffer that has not :CoqStarted yet.
@whonore
Copy link
Owner

whonore commented Aug 11, 2024

I worried something like that might be possible. Is this something you came across accidentally during normal use or did you trigger it intentionally by spamming :CoqToLine?

@tomtomjhj
Copy link
Contributor Author

I think I accidentally pressed my mappings for CoqUndo (<C-M-k>) and CoqToLine (<C-M-l>) at the same time

whonore added a commit that referenced this issue Aug 23, 2024
@whonore
Avoid race condition while starting coqtail
b50e57b 
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.
@whonore whonore mentioned this issue Aug 23, 2024
Merged
whonore added a commit that referenced this issue Aug 23, 2024
@whonore
Avoid race condition while starting coqtail
77f55bc 
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Avoid race condition while starting coqtail whonore/Coqtail
2 participants
@whonore @tomtomjhj