whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 34 forks source link

race between coqtail#start and CoqToLine #364

Closed tomtomjhj closed 3 months ago

tomtomjhj commented 3 months ago

After ac6e91f72c43ea5b7734daca160f8072b6e98799, 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 commented 3 months ago

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 commented 3 months ago

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