Failed to launch Coq in wsl

[PROgram52bc]

I am having trouble starting coqtail in vim under Windows WSL2.

$ coqtop --version
The Coq Proof Assistant, version 8.13.2 (December 2021)
compiled on Dec 26 2021 19:55:58 with OCaml 4.13.1

$ vim --version
VIM - Vi IMproved 8.1 (2018 May 18, compiled Apr 15 2020 06:40:31)
Included patches: 1-2269
Modified by team+vim@tracker.debian.org
Compiled by team+vim@tracker.debian.org
Huge version without GUI.  Features included (+) or not (-):
+acl               -farsi             -mouse_sysmouse    -tag_any_white
+arabic            +file_in_path      +mouse_urxvt       -tcl
+autocmd           +find_in_path      +mouse_xterm       +termguicolors
+autochdir         +float             +multi_byte        +terminal
-autoservername    +folding           +multi_lang        +terminfo
-balloon_eval      -footer            -mzscheme          +termresponse
+balloon_eval_term +fork()            +netbeans_intg     +textobjects
-browse            +gettext           +num64             +textprop
++builtin_terms    -hangul_input      +packages          +timers
+byte_offset       +iconv             +path_extra        +title
+channel           +insert_expand     -perl              -toolbar
+cindent           +job               +persistent_undo   +user_commands
-clientserver      +jumplist          +postscript        +vartabs
-clipboard         +keymap            +printer           +vertsplit
+cmdline_compl     +lambda            +profile           +virtualedit
+cmdline_hist      +langmap           -python            +visual
+cmdline_info      +libcall           +python3           +visualextra
+comments          +linebreak         +quickfix          +viminfo
+conceal           +lispindent        +reltime           +vreplace
+cryptv            +listcmds          +rightleft         +wildignore
+cscope            +localmap          -ruby              +wildmenu
+cursorbind        -lua               +scrollbind        +windows
+cursorshape       +menu              +signs             +writebackup
+dialog_con        +mksession         +smartindent       -X11
+diff              +modify_fname      +sound             -xfontset
+digraphs          +mouse             +spell             -xim
-dnd               -mouseshape        +startuptime       -xpm
-ebcdic            +mouse_dec         +statusline        -xsmp
+emacs_tags        +mouse_gpm         -sun_workshop      -xterm_clipboard
+eval              -mouse_jsbterm     +syntax            -xterm_save
+ex_extra          +mouse_netterm     +tag_binary
+extra_search      +mouse_sgr         -tag_old_static
   system vimrc file: "$VIM/vimrc"
     user vimrc file: "$HOME/.vimrc"
 2nd user vimrc file: "~/.vim/vimrc"
      user exrc file: "$HOME/.exrc"
       defaults file: "$VIMRUNTIME/defaults.vim"
  fall-back for $VIM: "/usr/share/vim"
Compilation: gcc -c -I. -Iproto -DHAVE_CONFIG_H   -Wdate-time  -g -O2 -fdebug-prefix-map=/build/vim-iU6mZD/vim-8.1.2269=. -fstack-protector-strong -Wformat -Werror=format-security -D_REENTRANT -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=1
Linking: gcc   -Wl,-Bsymbolic-functions -Wl,-z,relro -Wl,-z,now -Wl,--as-needed -o vim        -lm -ltinfo -lnsl  -lselinux  -lcanberra -lacl -lattr -lgpm -ldl     -L/usr/lib/python3.8/config-3.8-x86_64-linux-gnu -lpython3.8 -lcrypt -lpthread -ldl -lutil -lm -lm

When I execute :CoqStart with debugging information enbaled, I get Failed to launch Coq. Here is the log information I get

2021-12-26 23:05:33,241: start
2021-12-26 23:05:33,538: ('/mnt/c/Users/david/.linux/.opam/ocaml-base-compiler.4.13.1/bin/coqidetop', '-main-channel', 'stdfds', '-async-proofs', 'on', '-async-proofs-command-error-resilience', 'off', '-async-proofs-tactic-error-resilience', 'off', '-topfile', '/mnt/c/Users/david/.linux/foo.v')
2021-12-26 23:05:33,644: <?xml version="1.0" ?>
<call val="Init">
    <option val="none"/>
</call>

2021-12-26 23:05:41,915: <?xml version="1.0" ?>
<response>
    <value val="good">
        <state_id val="1"/>
    </value>
</response>

2021-12-26 23:05:41,915: stop

[whonore]

Thanks for reporting. Could you try adding print(ver_or_err, stderr) to line 199 of python/coqtail.py, just before the return, and tell me what it says when you run :CoqStart?

[PROgram52bc]

Thanks for reporting. Could you try adding print(ver_or_err, stderr) to line 199 of python/coqtail.py, just before the return, and tell me what it says when you run :CoqStart?

It says {'version': (8, 13, 2), 'str_version': '8.13.2', 'latest': None}.

Also, I tried doing the samething with neovim 0.7, and coqtail was able to start successfully. So I guess it has to do with the vim version I was using. I don't know what configuration causes it to break, though.

[whonore]

It seems like there may be something wrong with the Vim-Python channel. Could you try :call ch_logfile('coqtail.log', 'w') before :CoqStart and posting the contents of coqtail.log here?

[PROgram52bc]

It seems like there may be something wrong with the Vim-Python channel. Could you try :call ch_logfile('coqtail.log', 'w') before :CoqStart and posting the contents of coqtail.log here?

==== start log session ==== 0.000040 : SafeState: Start triggering 0.000830 : looking for messages on channels 0.001041 : SafeState: back to waiting, triggering SafeStateAgain 0.301826 : SafeState: reset: key typed 0.303055 SEND on 0(in): '[0,["highlight",[]]] ' 0.318158 RECV on 0(out): '["call","coc#api#call",["eval",["[bufnr(\"%\"),win_getid(),coc#cursor#position(),get(b:,'coc_cursors_activated',0)]"]],-10] ' 0.337173 SEND on 0(in): '[0,["CocAutocmd",["CursorHold",1]]] ' 0.337717 : SafeState: Start triggering 0.338304 : looking for messages on channels 0.338457 on 0: Calling 'coc#api#call' 0.349284 SEND on 0(in): '[-10,[null,[1,1000,[0,0],0]]] ' 0.349426 : SafeState: back to waiting, triggering SafeStateAgain 0.639327 : looking for messages on channels 0.640374 : SafeState: back to waiting, triggering SafeStateAgain 1.120760 : SafeState: reset: key typed 1.121177 : SafeState: Start triggering 1.121391 : looking for messages on channels 1.121561 : SafeState: back to waiting, triggering SafeStateAgain 2.327295 : SafeState: reset: key typed 2.327652 : SafeState: Start triggering 2.328021 : looking for messages on channels 2.328360 : SafeState: back to waiting, triggering SafeStateAgain 2.682207 : SafeState: reset: key typed 2.682592 : SafeState: Start triggering 2.682793 : looking for messages on channels 2.682973 : SafeState: back to waiting, triggering SafeStateAgain 2.683151 : SafeState: reset: key typed 2.683308 : SafeState: Start triggering 2.683505 : looking for messages on channels 2.683641 : SafeState: back to waiting, triggering SafeStateAgain 2.994760 : SafeState: reset: key typed 2.995180 : SafeState: Start triggering 2.995384 : looking for messages on channels 2.995671 : SafeState: back to waiting, triggering SafeStateAgain 3.276232 : SafeState: reset: key typed 3.276599 : SafeState: Start triggering 3.276760 : looking for messages on channels 3.276921 : SafeState: back to waiting, triggering SafeStateAgain 3.408183 : SafeState: reset: key typed 3.408462 : SafeState: Start triggering 3.408789 : looking for messages on channels 3.409042 : SafeState: back to waiting, triggering SafeStateAgain 3.639441 : SafeState: reset: key typed 3.639694 : SafeState: Start triggering 3.639901 : looking for messages on channels 3.640172 : SafeState: back to waiting, triggering SafeStateAgain 3.962019 : SafeState: reset: ins_typebuf() 3.962390 : SafeState: Start triggering 3.962547 : looking for messages on channels 3.962718 : SafeState: back to waiting, triggering SafeStateAgain 4.016228 : SafeState: reset: key typed 4.016669 : SafeState: Start triggering 4.016896 : looking for messages on channels 4.017148 : SafeState: back to waiting, triggering SafeStateAgain 4.185875 : SafeState: reset: key typed 4.186237 : SafeState: Start triggering 4.186424 : looking for messages on channels 4.186587 : SafeState: back to waiting, triggering SafeStateAgain 4.246695 : SafeState: reset: key typed 4.247042 : SafeState: Start triggering 4.247244 : looking for messages on channels 4.247428 : SafeState: back to waiting, triggering SafeStateAgain 4.410007 : SafeState: reset: ins_typebuf() 4.410452 : SafeState: Start triggering 4.410628 : looking for messages on channels 4.410801 : SafeState: back to waiting, triggering SafeStateAgain 4.878053 : SafeState: reset: key typed 4.937761 on 1: Created channel 4.937954 on 1: Connecting to localhost port 57781 4.938560 on 1: Waiting for connection (waiting 1 msec)... 4.938716 on 1: Connection made 4.945813 SEND on 0(in): '[0,["CocAutocmd",["BufWinLeave",1,1000]]] ' 4.947268 SEND on 0(in): '[0,["CocAutocmd",["BufHidden",1]]] ' 5.020919 SEND on 0(in): '[0,["CocAutocmd",["BufCreate",2]]] ' 5.054772 RECV on 0(out): '["call","coc#api#call",["call_function",["coc#util#get_bufoptions",[2,10485760]]],-11] ' 5.061275 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",2]]] ' 5.064766 SEND on 0(in): '[0,["CocAutocmd",["BufWinEnter",2,1000]]] ' 5.251732 SEND on 0(in): '[0,["CocAutocmd",["FileType","coq-goals",2]]] ' 5.260559 SEND on 0(in): '[0,["CocAutocmd",["BufWinLeave",2,1000]]] ' 5.261379 SEND on 0(in): '[0,["CocAutocmd",["BufHidden",2]]] ' 5.298881 SEND on 0(in): '[0,["CocAutocmd",["BufCreate",3]]] ' 5.301260 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",3]]] ' 5.302080 RECV on 0(out): '["call","coc#api#call",["call_function",["coc#util#get_bufoptions",[3,10485760]]],-12] ' 5.304741 SEND on 0(in): '[0,["CocAutocmd",["BufWinEnter",3,1000]]] ' 5.491088 SEND on 0(in): '[0,["CocAutocmd",["FileType","coq-infos",3]]] ' 5.494555 SEND on 0(in): '[0,["CocAutocmd",["BufWinLeave",3,1000]]] ' 5.495232 SEND on 0(in): '[0,["CocAutocmd",["BufHidden",3]]] ' 5.495796 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",1]]] ' 5.498890 SEND on 0(in): '[0,["CocAutocmd",["BufWinEnter",1,1000]]] ' 5.536543 SEND on 0(in): '[0,["CocAutocmd",["WinLeave",1000]]] ' 5.541145 SEND on 0(in): '[0,["CocAutocmd",["WinEnter",1001]]] ' 5.542260 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",2]]] ' 5.546913 SEND on 0(in): '[0,["CocAutocmd",["BufWinEnter",2,1001]]] ' 5.549023 SEND on 0(in): '[0,["CocAutocmd",["WinLeave",1001]]] ' 5.553472 SEND on 0(in): '[0,["CocAutocmd",["WinEnter",1000]]] ' 5.553903 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",1]]] ' 5.554429 SEND on 0(in): '[0,["CocAutocmd",["WinLeave",1000]]] ' 5.558912 SEND on 0(in): '[0,["CocAutocmd",["WinEnter",1001]]] ' 5.560076 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",2]]] ' 5.560440 SEND on 0(in): '[0,["CocAutocmd",["WinLeave",1001]]] ' 5.566634 SEND on 0(in): '[0,["CocAutocmd",["WinEnter",1002]]] ' 5.568340 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",3]]] ' 5.574517 SEND on 0(in): '[0,["CocAutocmd",["BufWinEnter",3,1002]]] ' 5.576973 SEND on 0(in): '[0,["CocAutocmd",["WinLeave",1002]]] ' 5.583291 SEND on 0(in): '[0,["CocAutocmd",["WinEnter",1000]]] ' 5.584193 SEND on 0(in): '[0,["CocAutocmd",["BufEnter",1]]] ' 5.612153 SEND on 1(sock): '[1,[1,"start",{"args":[],"coq_prog":"","coqpath":"","opts":{"timeout":0,"filename":"/mnt/c/Users/david/.linux/.vim/bundle/Coqtail/python/a.v","encoding":"utf-8"}}]] ' 5.612398 on 1: Blocking read JSON for id 1 5.612613 : looking for messages on channels 5.612893 on 0: Calling 'coc#api#call' 5.613690 SEND on 0(in): '[-11,[null,{"changedtick":2,"variables":{},"winid":1001,"eol":1,"previewwindow":false,"bufname":"Goal0","fullpath":"/mnt/c/Users/david/.linux/.vim/bundle/Coqtail/python/Goal0","filetype":"coq-goals","buftype":"nofile","lines":[],"iskeyword":"@,48-57,192-255,,'","size":-1}]] ' 5.614063 on 0: Calling 'coc#api#call' 5.615001 SEND on 0(in): '[-12,[null,{"changedtick":2,"variables":{},"winid":1002,"eol":1,"previewwindow":false,"bufname":"Info0","fullpath":"/mnt/c/Users/david/.linux/.vim/bundle/Coqtail/python/Info0","filetype":"coq-infos","buftype":"nofile","lines":[],"iskeyword":"@,48-57,192-255,_,'","size":-1}]] ' 5.615242 : looking for messages on channels 5.615427 on 1: Waiting for up to 5000 msec 10.620634 on 1: Timed out on id 1 10.621589 SEND on 1(sock): '[2,[1,"stop",{"opts":{"timeout":0,"filename":"/mnt/c/Users/david/.linux/.vim/bundle/Coqtail/python/a.v","encoding":"utf-8"}}]] ' 10.621827 on 1: Blocking read JSON for id 2 10.622035 : looking for messages on channels 10.622413 on 1: Waiting for up to 5000 msec 15.627696 on 1: Timed out on id 2 15.628497 : ERROR silent: E216: No such group or event: coqtail#Sync * 15.628717 on 1: Closing channel 15.628992 on 1: Clearing channel 15.629363 SEND on 0(in): '[0,["CocAutocmd",["BufWinLeave",2,1001]]] ' 15.630304 SEND on 0(in): '[0,["CocAutocmd",["BufHidden",2]]] ' 15.631041 RECV on 0(out): '["call","coc#api#call",["eval",["[win_getid(),bufnr('%'),coc#window#find('cocViewId', 'OUTLINE')]"]],-13] ' 15.635085 SEND on 0(in): '[0,["CocAutocmd",["BufUnload",2]]] ' 15.636051 SEND on 0(in): '[0,["CocAutocmd",["BufWinLeave",3,1002]]] ' 15.636663 SEND on 0(in): '[0,["CocAutocmd",["BufHidden",3]]] ' 15.639783 SEND on 0(in): '[0,["CocAutocmd",["BufUnload",3]]] ' 15.640540 : SafeState: Start triggering 15.645613 : SafeState: reset: key typed 15.645934 : Exiting... 15.646166 SEND on 0(in): '[0,["CocAutocmd",["BufWinLeave",1,1000]]] ' 15.647578 SEND on 0(in): '[0,["CocAutocmd",["BufUnload",1]]] '

[whonore]

Maybe coc is interfering somehow? What happens if you disable that plugin?

[PROgram52bc]

==== start log session ==== 0.000015 : SafeState: Start triggering 0.000728 : looking for messages on channels 0.000941 : SafeState: back to waiting, triggering SafeStateAgain 0.301952 : SafeState: reset: key typed 0.302863 : ERROR silent: E117: Unknown function: CocActionAsync 0.304332 : SafeState: Start triggering 0.306018 : looking for messages on channels 0.306641 : SafeState: back to waiting, triggering SafeStateAgain 1.044791 : SafeState: reset: key typed 1.045195 : SafeState: Start triggering 1.045367 : looking for messages on channels 1.045489 : SafeState: back to waiting, triggering SafeStateAgain 1.406504 : SafeState: reset: key typed 1.406724 : SafeState: Start triggering 1.406925 : looking for messages on channels 1.407251 : SafeState: back to waiting, triggering SafeStateAgain 1.752573 : SafeState: reset: key typed 1.753118 : SafeState: Start triggering 1.753282 : looking for messages on channels 1.753475 : SafeState: back to waiting, triggering SafeStateAgain 2.087880 : SafeState: reset: key typed 2.088265 : SafeState: Start triggering 2.088499 : looking for messages on channels 2.088694 : SafeState: back to waiting, triggering SafeStateAgain 2.398766 : SafeState: reset: key typed 2.399121 : SafeState: Start triggering 2.399324 : looking for messages on channels 2.399590 : SafeState: back to waiting, triggering SafeStateAgain 2.705870 : SafeState: reset: key typed 2.706370 : SafeState: Start triggering 2.706595 : looking for messages on channels 2.706926 : SafeState: back to waiting, triggering SafeStateAgain 4.239244 : SafeState: reset: key typed 4.285673 on 0: Created channel 4.285825 on 0: Connecting to localhost port 40947 4.286067 on 0: Waiting for connection (waiting 1 msec)... 4.286307 on 0: Connection made 4.779124 SEND on 0(sock): '[1,[1,"start",{"args":[],"coq_prog":"","coq_path":"","opts":{"timeout":0,"filename":"/mnt/c/Users/david/.linux/a.v","encoding":"utf-8"}}]] ' 4.779285 on 0: Blocking read JSON for id 1 4.779550 : looking for messages on channels 4.779711 on 0: Waiting for up to 5000 msec 9.784967 on 0: Timed out on id 1 9.785786 SEND on 0(sock): '[2,[1,"stop",{"opts":{"timeout":0,"filename":"/mnt/c/Users/david/.linux/a.v","encoding":"utf-8"}}]] ' 9.786096 on 0: Blocking read JSON for id 2 9.786286 : looking for messages on channels 9.786639 on 0: Waiting for up to 5000 msec 14.791143 on 0: Timed out on id 2 14.792022 : ERROR silent: E216: No such group or event: coqtail#Sync * 14.792159 on 0: Closing channel 14.792366 on 0: Clearing channel 14.811004 : SafeState: Start triggering 14.819727 : SafeState: reset: key typed 14.819945 : Exiting...

[whonore]

Ok, so coc seems unrelated. Vim is successfully sending a message to Python, but it's not receiving the response. Try adding prints to python/coqtail.py at lines 865 and 867 to confirm the response is being sent. Something like:

try:
    ret = handler(**args) if handler is not None else None
    msg = [self.msg_id, {"buf": self.bnum, "ret": ret}]
    print(msg)
    self.wfile.write(_to_jsonl(msg))
except (EOFError, ConnectionError) as e:
    print(str(e))
    break

[PROgram52bc]

I got this:

[1, {'buf': 1, 'ret': ({'version': (8, 13, 2), 'str_version': '8.13.2', 'latest': None}, '')}]

[whonore]

So it looks like the Python side is sending the response, it's just never received for some reason. Thanks for your help so far but it looks like I'll probably need to do some debugging on my Windows machine, which unfortunately I won't have access to for a few weeks.

In the meantime if neovim works I'd suggest sticking with that for now. Feel free to keep digging into this if you're interested, but I don't have any ideas at the moment for an obvious next place to look.

[whonore]

I finally got around to trying this on WSL and unfortunately I'm not able to reproduce it. So I think I'm stuck unless someone else runs into this and we can get more information about what's going on.

[dcgrigsby]

After resolving #316 , I saw this issue. In my case, I was able to resolve it. I had set the b:coqtail_coq_path and b:coqtail_coq_prog variables (to `/usr/bin/' and 'coqtop' respectively). It produced this error:

Failed to launch Coq.
Coqtail experienced an unexpected error. Please report at https://github.com/whonore/Coqtail/issues.
Welcome to Coq 8.15.0

Seeing the welcome message surprised me. Removing it altogether (because coq is in the path) resolved it for me, anyway.