search

whonore / Coqtail

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

Failed to launch Coq. #241

Open vsiles opened 3 years ago

vsiles commented 3 years ago

Hi ! I'm getting this message for a few days now (didn't change anything. Same version of vim/plugin/opam/ocaml/coq).

It seems to randomly start (and once started, it works alright).

I don't know how to get more diagnostic or try to debug this. How can I get more information on what failed ?

OS: MacOS Monterey 12.0.1 vim: VIM - Vi IMproved 8.2 (2019 Dec 12, compiled Sep 16 2020 23:47:44) opam: 2.0.6 ocaml: 4.12.0 coq: 8.13.2

vsiles commented 3 years ago

In case it helped, I tried to use :set verbose=15 and I'm seeing some Exception caught: Vim(return):E121: Undefined variable: b:coqtail_panel_bufs, or this

chdir(/Users/vsiles/.vim/bundle/Coqtail/autoload/coqtail)
fchdir() to previous dir
line 15: sourcing "/Users/vsiles/.vim/bundle/Coqtail/autoload/coqtail/util.vim"
finished sourcing /Users/vsiles/.vim/bundle/Coqtail/autoload/coqtail/util.vim
continuing in coqtail#start
                           Failed to launch Coq.
Error detected while processing function coqtail#start[29]..coqtail#stop[2]..<SNR>31_cleanup:
line    6:
E216: No such group or event: coqtail#Sync * <buffer>
Error detected while processing function coqtail#start[29]..coqtail#stop[2]..<SNR>31_cleanup[9]..<SNR>36_close:
line    1:
E906: not an open channel

Executing VimLeavePre Autocommands for "*"
autocommand call py3eval('CoqtailServer.stop_server()') | let s:port = -1

Writing viminfo file "/Users/vsiles/.viminfo"

Here is the log generated by vim -V9myVim.log foo.v (empty non existing file) with only :CoqStart && :q, no other plugin than CoqTail myVim.log :

vsiles commented 3 years ago

In case of doubt, reboot... Now things looks ok. I'll monitor this today. Please tell me if anything in the log looks suspicious

whonore commented 3 years ago

Thanks for the detailed report. Nothing stands out to me in the log, but if it starts happening again running :CoqToggleDebug before :CoqStart will log the XML communication between Coqtail and Coq so that might give some more hints as to what's going on. Since there's no additional message after "Failed to launch Coq." it seems like it maybe isn't able to communicate with Coq at all so I'm wondering if maybe this is a similar problem to #154 or #239 where some configuration issue is blocking Coqtail from binding a port or opening a socket.

vsiles commented 3 years ago

No problem today either. I really feel something was wrong with my mac and reboot fixed it. I did tried to do CoqToggleDebug but I didn't see much. Where is located its output ?

Closing as it is more likely a mac issue that CoqTail.

whonore commented 3 years ago

Glad it's working now. Feel free to reopen if it happens again.

I did tried to do CoqToggleDebug but I didn't see much. Where is located its output ?

It creates a temporary file whose path is stored in b:coqtail_log_name.

vsiles commented 2 years ago

Happened again today (after only one day of uptime). I tried let b:coqtail_log_name = "/tmp/foo" and :CoqToogleDebug but it didn't log anything. Rebooting solved the issue, but I'd like to understand what's happening to find another work around. Do you have any idea what might be the issue ? Maybe left over pipes/lock files ?

whonore commented 2 years ago

I tried let b:coqtail_log_name = "/tmp/foo" and :CoqToogleDebug but it didn't log anything.

Sorry, what I meant is :CoqToggleDebug will automatically create a temporary log and store the path in b:coqtail_log_name.

Maybe left over pipes/lock files ?

Something like that is definitely possible. Something I suggested before to help diagnose a similar problem was, when you start encountering the problem, run python -c 'from socketserver import *; s = ThreadingTCPServer(("localhost", 0), StreamRequestHandler); print(s.server_address); s.serve_forever()' and then use nmap or something to see if the port is open or if you can connect to it.

If that part's working and the debug log doesn't show anything useful then my only other thought is to sprinkle print statements around to pinpoint where the failure is happening. If it comes to that I can suggest some places to put them.

Does this issue start the first time you try to use Coqtail after reboot, or does it work for a while and then suddenly stop launching the next time you try?

vsiles commented 2 years ago

it works for a (random) while and stops working. reboot fixes it I'll try the python thing next time I have issues.

vsiles commented 2 years ago

It's happening again, I'm investigating:

I never used vimscript or plugin, so any advice on where to add print and how to trigger them would be helpful for next time. I'll reboot in a few minutes to be able to work :D

whonore commented 2 years ago

The log path is in b:coqtail_log_name, not b:coqtail_log_path.

As for printing a good place to start is Coqtop.start in python/coqtop.py. Specifically the following lines:

Additionally on Line 195 of Coqtail.start in python/coqtail.py printing ver_or_err and stderr will show the result of Coqtop.start.

Finally on Line 329 of coqtail#start in autoload/coqtail.vim printing l:ok (with :echom) could indicate if the error is on the Coq side or if there's a problem with the Vim-Python communication channel.

vsiles commented 2 years ago

None of my print in python code showed up. I tried line 329 of coqtail.vim and it shows l:ok = 0 and l:ver_or_msg = -1. I'll try to dump more from this file to try and understand what's happening

vsiles commented 2 years ago

I left vim/coq for a meeting and when I was back, I managed to run Coqtail correctly, and now it won't start again. Still more questions :D

whonore commented 2 years ago

Since l:ok = 0 that makes me think something is going wrong with the Vim-Python channel. Try doing :call ch_logfile('coqtail.log', 'w') before :CoqStart. That will make Vim log all the channel communication in coqtail.log (or whatever filename you choose). Maybe something is causing it to close prematurely?

vsiles commented 2 years ago 
 2.284186 : raw key input: "t"
 46   2.284253 : SafeState: reset: key typed
 47   2.284293 : SafeState: Start triggering
 48   2.284391 : looking for messages on channels
 49   2.284430 : SafeState: back to waiting, triggering SafeStateAgain
 50   2.501145 : raw key input: "^M"
 51   2.501234 : SafeState: reset: key typed
 52   2.501605 on 4: Created channel
 53   2.502273 on 4: Resolved localhost to ::1
 54   2.502309 on 4: Trying to connect to ::1 port 62387
 55   2.502377 on 4: Connecting...
 56   2.502486 on 4: Waiting for connection (waiting 1 msec)...
 57   2.502568 ERR on 4: Connection timed out
 58   2.502603 on 4: Resolved localhost to 127.0.0.1
 59   2.502616 on 4: Trying to connect to 127.0.0.1 port 62387
 60   2.502649 on 4: Connecting...
 61   2.502714 on 4: Waiting for connection (waiting 1 msec)...
 62   2.504027 ERR on 4: Connection timed out
 63   2.720775 : ERROR silent: E216: No such group or event: coqtail#Sync * <buffer>
 64   2.720814 : ERROR silent: E906: not an open channel
 65   2.743618 : SafeState: Start triggering
 66   2.772226 : looking for messages on channels
 67   2.772269 on 4: Closing channel because all readable fds are closed
 68   2.772294 on 4: Closing channel
 69   2.772323 on 4: Closing channel
 70   2.772332 on 4: Clearing channel
 71   2.772341 on 4: Freeing channel
 72   2.772349 : SafeState: back to waiting, triggering SafeStateAgain
 73   3.451334 : raw key input: ":"

this should be informative

whonore commented 2 years ago

Ok so the problem is Vim isn't able to connect to the Python server. That's either because the server is going down or something is blocking the connection. I just merged a change that will print a bit more information about this error. If you pull the most recent version then next time it happens you should see "Failed to connect to Coqtail server at port {p}.". Then, with Vim still open, try connecting to that port (e.g., nc -zv localhost {p}). If it connects then the Python server is running and Vim is being blocked for some reason. If it doesn't then something is forcing the server to shut down prematurely.

vsiles commented 2 years ago

Nice addition, thank you

$ nc -zv localhost 62352
nc: connectx to localhost port 62352 (tcp) failed: Connection refused
Connection to localhost port 62352 [tcp/*] succeeded!

I'm not familiar with port debugging, I'll see what I can find

EDIT1:

$ netstat -la # on macos...
tcp4       0      0  localhost.62352                               *.*                                           LISTEN
sudo lsof -i -P | grep LISTEN | grep 62352
$ vim       54417         vsiles    3u  IPv4 0x42e9e405b5b413cb      0t0    TCP localhost:62352 (LISTEN)

This is the vim I have opened and where :CoqStart failed

If I close it, nothing is reported anymore and

$ nc -zv localhost 62352
nc: connectx to localhost port 62352 (tcp) failed: Connection refused
nc: connectx to localhost port 62352 (tcp) failed: Connection refused
whonore commented 2 years ago

So it looks like the server is up, but the Vim channel is timing out when connecting to it. I'm not really sure where to go from here. A somewhat similar issue was fixed by doing something to /etc/hosts, but in that case :CoqStart was failing consistently, not after a random period of time.

Just as a sanity check, when it starts failing, with Vim still open (so the Python server doesn't shut down), try :echo ch_status(ch_open('localhost:{p}')) where {p} is the port reported by the error message. It should print fail. You could also try increasing the connection timeout with :echo ch_status(ch_open('localhost:{p}', {"waittime": 10})).

vsiles commented 2 years ago

I just tried the two :echo commands. They indeed return fail. I tried with bigger waittime, up to 6000 and it still fail.

I waited a bit with vim still opened. Tried again a couple times and at some point it worked once more.. really I don't understand :D

whonore commented 2 years ago

It's very strange and unfortunately I'm out of debugging ideas. I'll leave this issue open in case someone encounters the same problem or if there are new developments.

As a workaround you might try using NeoVim. Coqtail uses a slightly different approach for the NeoVim-Python communication so maybe it won't have this same issue.

vsiles commented 2 years ago

Never used NeoVim, that might be a good opportunity to do so ;) Thanks a lot for the support. I'll only update if I get meaningful info to debug.

vsiles commented 2 years ago

I installed neovim today. I have a setup where vim can't start the plugin but nvim is fine :D I'll monitor if nvim ever fails (they share the same config/plugin)

AlexHYF commented 9 months ago

I am encountering the same issue. With Vim 9.15 on M1 Mac mini

I fixed it by restarting my Mac. It might be a problem with OSX

whonore commented 9 months ago

Sorry to hear this is still going on. I don't have a Mac to test with, but I'm happy to help as best I can if you think of any other ways of diagnosing the problem.