coq-au-vim issueshttps://framagit.org/manu/coq-au-vim/-/issues2020-04-28T06:32:09Zhttps://framagit.org/manu/coq-au-vim/-/issues/1[Feature Request] Support for _CoqProject file2020-04-28T06:32:09ZVirgile Robles[Feature Request] Support for _CoqProject fileHello and thank you for your great plugin.
I'm using it to follow Pierce's Software Foundation courses and it seems the latest version uses a _CoqProject file (as defined here: https://coq.inria.fr/refman/practical-tools/utilities.html#b...Hello and thank you for your great plugin.
I'm using it to follow Pierce's Software Foundation courses and it seems the latest version uses a _CoqProject file (as defined here: https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile) to organize modules.
It would be great if coq-au-vim had native support for this file, as it is somewhat tedious to tweak every file so that it will work within vim.
Best regards.https://framagit.org/manu/coq-au-vim/-/issues/5E716: Key not present in Dictionary: zones E15: Invalid expression: self.zones2019-05-20T07:49:30ZBartłomiej PugetE716: Key not present in Dictionary: zones E15: Invalid expression: self.zonesHi, I tried to run your plugin with:
* Vim 8.1
* Coq 8.6
I receive following errors when executing eg. `:CoqNext` (`:CoqStart` didn't report any problems):
```
Error detected while processing function 322[3]..305:
line 8:
E716...Hi, I tried to run your plugin with:
* Vim 8.1
* Coq 8.6
I receive following errors when executing eg. `:CoqNext` (`:CoqStart` didn't report any problems):
```
Error detected while processing function 322[3]..305:
line 8:
E716: Key not present in Dictionary: zones
E15: Invalid expression: self.zones
```
Minimal workaround that works for me (I didn't have time to fully understand what is going on here):
```
autoload/coqtop.vim | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/autoload/coqtop.vim b/autoload/coqtop.vim
index 6239c8d..635fe84 100644
--- a/autoload/coqtop.vim
+++ b/autoload/coqtop.vim
@@ -537,7 +537,7 @@ function s:coq.try_start (job, status)
endif
" Try to start using the next potential command.
- let cmd = remove(self.job_commands, 0) . ' -main-channel stdfds -async-proofs on'
+ let cmd = remove(self.job_commands, 1) . ' -main-channel stdfds -async-proofs on'
call self.log('j', "start", cmd)
let self.job = job_start(cmd,
\ {'mode': 'raw', 'out_cb': self.callback, 'exit_cb': self.try_start})
```https://framagit.org/manu/coq-au-vim/-/issues/3Initialisation hangs when using coqtop2019-05-20T07:50:38ZAdam MatoušekInitialisation hangs when using coqtopThere is a race condition when launching a Coq toplevel during `:CoqStart`. It manifests probably only with older Coq, i.e. when `coqtop` (v. 8.6) is needed instead of `coqidetop` (v. 8.9). I suspect it happens like this:
1. A job with ...There is a race condition when launching a Coq toplevel during `:CoqStart`. It manifests probably only with older Coq, i.e. when `coqtop` (v. 8.6) is needed instead of `coqidetop` (v. 8.9). I suspect it happens like this:
1. A job with `coqidetop` is created.
2. (I tried to call `job_status()` here, which checks the running/dead status of a job, but since the job probably only managed to `fork` and not yet `execv`, it still appears fine.)
3. The initialisation script continues, reaching the point where an “About” call is made to the `coqidetop` job.
4. (Sometimes, with debug options set, it fails here, as the channel being written to is already closed, but more often this does not happen on my machine.)
5. The call's XML is written to the channel, which still appears fine.
6. The job finally gets to `execv` `coqidetop`, which I do not have.
7. The job exits, calling the callback which in turn launches a job with the older `coqtop`.
8. The `coqtop` job starts correctly, but the “About” call is trapped in the first job's channel (or perhaps even consumed and buffered by the now-dead job, I am not sure if that is possible). As it never reaches `coqtop`, the script never receives a response and the initialisation does not continue.
I spent several hours trying to fix this issue in an elegant way, but to no avail. For now, I just wait 100ms after the first job is launched, which is of course a dirty work-around and not at all an actual solution. Using the same channel for both jobs might be worth looking into, although I do not know, whether the first job would not consume any input before exiting. Another variant might be checking whether `coqidetop` exists beforehand and launching the correct toplevel right away.
Introduced by: 1ff3c89bhttps://framagit.org/manu/coq-au-vim/-/issues/2Neovim support2023-10-23T17:57:40ZRalf VoglerNeovim supportRunning with `vim` works, but with `nvim` I get the following errors upon `:CoqStart`. I don't know if it's easy to adjust.
~~~
Error detected while processing function coqtop#Start[1]..158[21]..127:
line 2:
E121: Undefined variable:...Running with `vim` works, but with `nvim` I get the following errors upon `:CoqStart`. I don't know if it's easy to adjust.
~~~
Error detected while processing function coqtop#Start[1]..158[21]..127:
line 2:
E121: Undefined variable: v:none
E116: Invalid arguments for function 128
Error detected while processing function coqtop#Start[1]..158[22]..133[2]..130:
line 3:
E716: Key not present in Dictionary: return_queue, [a:command, a:000, a:callback, a:dict])
E116: Invalid arguments for function add
line 4:
E716: Key not present in Dictionary: channel, xml)
E116: Invalid arguments for function ch_sendraw
~~~
* Coq version (run `coqtop -v` if unsure): 8.9.0 (February 2019)
* Neovim version (run `nvim -v` if unsure): v0.3.5https://framagit.org/manu/coq-au-vim/-/issues/7Plugin breaks on Coq 8.19 rather than report protocol error2024-03-25T10:46:24ZIsaac van BakelPlugin breaks on Coq 8.19 rather than report protocol errorI recently upgraded to Coq 8.19 for a project, and when trying to use the plugin I expected to get a standard protocol error due to the bump in protocol version. (This Coq version also comes with some optional additional XML info, see [h...I recently upgraded to Coq 8.19 for a project, and when trying to use the plugin I expected to get a standard protocol error due to the bump in protocol version. (This Coq version also comes with some optional additional XML info, see [here](https://coq.inria.fr/doc/V8.19.0/refman/changes.html#id264).)
Instead, I found that the plugin simply succeeded on startup after exchanging some messages with the Coq server, and then broke when I tried to use it, with the following error:
```
Error detected while processing function 320[13]..function 320[3]..302:
line 8:
E716: Key not present in Dictionary: "zones"
```
Adding the protocol version to the list of supported versions fixes the above error and allows the plugin to work normally.
Here's an example log with `g:coq_debug = 'xermj'`:
```
j|start | coqidetop -main-channel stdfds -async-proofs on -Q <files>
j|started | process 3009 run channel 0 open
r|call | about
x|send | <call val="About"><unit/></call>
j|send | Vim(call):E631: ch_sendraw(): Write failed
j|failed |
j|start | coqidetop.opt -main-channel stdfds -async-proofs on -Q <files>
j|started | process 3010 run channel 1 open
r|call | about
x|send | <call val="About"><unit/></call>
x|recv | <value val="good"><coq_info><string>8.19.0</string><string>20230413</string><string>n/a</string><string>n/a</string></coq_info></value>
x|item | ['value', {'val': 'good'}, ['coq_info', {}, ['string', {}, '8.19.0'], ['string', {}, '20230413'], ['string', {}, 'n/a'], ['string', {}, 'n/a']]]
m|message | {'type': 'good', 'content': [['coq_info', {}, ['string', {}, '8.19.0'], ['string', {}, '20230413'], ['string', {}, 'n/a'], ['string', {}, 'n/a']]]}
r|good | {'version': '8.19.0', 'release': 'n/a', 'protocol': '20230413', 'success': 1, 'compile': 'n/a'}
x|recv | <feedback object="state" route="0"><state_id val="1"/><feedback_content val="workerstatus"><pair><string>proof:0:0</string><string>Idle</string></pair></feedback_content></feedback>
x|item | ['feedback', {'route': '0', 'object': 'state'}, ['state_id', {'val': '1'}], ['feedback_content', {'val': 'workerstatus'}, ['pair', {}, ['string', {}, 'proof:0:0'], ['string', {}, 'Idle']]]]
m|message | {'kind': 'workerstatus', 'type': 'feedback', 'state_id': '1', 'content': [['pair', {}, ['string', {}, 'proof:0:0'], ['string', {}, 'Idle']]]}
```https://framagit.org/manu/coq-au-vim/-/issues/6Plugin breaks on too-large coqide responses2023-08-09T11:42:06ZIsaac van BakelPlugin breaks on too-large coqide responsesIn some large Coq proofs, responses from the IDE server when using `:CoqNext` can exceed 65536 bytes in length, which causes them to be split over multiple callbacks from the perspective of coq-au-vim. This causes the plugin to become un...In some large Coq proofs, responses from the IDE server when using `:CoqNext` can exceed 65536 bytes in length, which causes them to be split over multiple callbacks from the perspective of coq-au-vim. This causes the plugin to become unusable for stepping through the proof, since it cannot parse the "partial" XML it receives in each callback (in particular, if a tag is split across two callbacks.)https://framagit.org/manu/coq-au-vim/-/issues/4plugin kills gvim after a few seconds of idle time2019-05-14T12:40:08ZPaul Sonkolyplugin kills gvim after a few seconds of idle timeHi all,
if I open a cock file, everything seems to work as expected, I can send code to coq and I get back the green/red highlight in short I think my setup is functional.
Except if I idle for a few seconds, gvim either freezes or abor...Hi all,
if I open a cock file, everything seems to work as expected, I can send code to coq and I get back the green/red highlight in short I think my setup is functional.
Except if I idle for a few seconds, gvim either freezes or aborts. This only happens if :CoqStart has been invoked and reproducible 100 %, although the freeze/abort varies, with freeze being more frequent.
I'm not sure how to debug this or gather more information but I tried running gvim from strace and the last bunch of lines before the freeze are as follows:
```
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc6d16ee000
rt_sigprocmask(SIG_UNBLOCK, [ABRT], NULL, 8) = 0
rt_sigprocmask(SIG_BLOCK, ~[RTMIN RT_1], [], 8) = 0
getpid() = 1169
gettid() = 1169
tgkill(1169, 1169, SIGABRT) = 0
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
--- SIGABRT {si_signo=SIGABRT, si_code=SI_TKILL, si_pid=1169, si_uid=1000} ---
rt_sigaction(SIGHUP, {sa_handler=SIG_IGN, sa_mask=[HUP], sa_flags=SA_RESTORER|SA_RESTART, sa_restorer=0x7fc6cfebb8b0}, {sa_handler=SIG_IGN, sa_mask=[], sa_flags=SA_RESTORER, sa_restorer=0x7fc6cfebb8b0}, 8) = 0
write(1, "Vim: Caught deadly signal ABRT\r\n", 32Vim: Caught deadly signal ABRT
) = 32
close(11) = 0
unlink("/home/phaul/.cache/vim/swap//%home%phaul%lf%Basics.v.swp") = 0
lstat("/tmp/vP8yiTR", {st_mode=S_IFDIR|0700, st_size=80, ...}) = 0
--- SIGSEGV {si_signo=SIGSEGV, si_code=SEGV_MAPERR, si_addr=0x28} ---
write(1, "Vim: Double signal, exiting\r\n", 29Vim: Double signal, exiting
) = 29
openat(AT_FDCWD, "/home/phaul/.viminfo", O_RDONLY) = 10
stat("/home/phaul/.viminfo", {st_mode=S_IFREG|0600, st_size=41371, ...}) = 0
getuid() = 1000
getuid() = 1000
stat("/home/phaul/.viminfo.tmp", {st_mode=S_IFREG|0600, st_size=25616, ...}) = 0
stat("/home/phaul/.viminfz.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfy.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfx.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfw.tmp", {st_mode=S_IFREG|0600, st_size=32787, ...}) = 0
stat("/home/phaul/.viminfv.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfu.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminft.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfs.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfr.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfq.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfp.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
stat("/home/phaul/.viminfo.tmp", {st_mode=S_IFREG|0600, st_size=25616, ...}) = 0
stat("/home/phaul/.viminfn.tmp", 0x7ffe8327cc50) = -1 ENOENT (No such file or directory)
umask(000) = 022
openat(AT_FDCWD, "/home/phaul/.viminfn.tmp", O_WRONLY|O_CREAT|O_EXCL|O_NOFOLLOW, 0600) = 11
umask(022) = 000
fcntl(11, F_GETFL) = 0x28001 (flags O_WRONLY|O_LARGEFILE|O_NOFOLLOW)
stat("/home/phaul/.viminfn.tmp", {st_mode=S_IFREG|0600, st_size=0, ...}) = 0
futex(0x7fc6d0043aa0, FUTEX_WAIT_PRIVATE, 2, NULL
```
note the SIGSEGV / SIGABRT received.
versions:
```
:version
VIM - Vi IMproved 8.1 (2018 May 18, compiled Apr 26 2019 21:55:55)
Included patches: 1-1186
Compiled by Arch Linux
Huge version with GTK3 GUI. Features included (+) or not (-):
+acl +cmdline_info -farsi +libcall -mouse_sysmouse +python3/dyn +termguicolors +vreplace
+arabic +comments +file_in_path +linebreak +mouse_urxvt +quickfix +terminal +wildignore
+autocmd +conceal +find_in_path +lispindent +mouse_xterm +reltime +terminfo +wildmenu
+autochdir +cryptv +float +listcmds +multi_byte +rightleft +termresponse +windows
-autoservername +cscope +folding +localmap +multi_lang +ruby/dyn +textobjects +writebackup
+balloon_eval +cursorbind -footer +lua/dyn -mzscheme +scrollbind +textprop +X11
+balloon_eval_term +cursorshape +fork() +menu +netbeans_intg +signs +timers -xfontset
+browse +dialog_con_gui +gettext +mksession +num64 +smartindent +title +xim
++builtin_terms +diff -hangul_input +modify_fname +packages +startuptime +toolbar -xpm
+byte_offset +digraphs +iconv +mouse +path_extra +statusline +user_commands +xsmp_interact
+channel +dnd +insert_expand +mouseshape +perl/dyn -sun_workshop +vartabs +xterm_clipboard
+cindent -ebcdic +job +mouse_dec +persistent_undo +syntax +vertsplit -xterm_save
+clientserver +emacs_tags +jumplist +mouse_gpm +postscript +tag_binary +virtualedit
+clipboard +eval +keymap -mouse_jsbterm +printer -tag_old_static +visual
+cmdline_compl +ex_extra +lambda +mouse_netterm +profile -tag_any_white +visualextra
+cmdline_hist +extra_search +langmap +mouse_sgr +python/dyn +tcl/dyn +viminfo
system vimrc file: "/etc/vimrc"
user vimrc file: "$HOME/.vimrc"
2nd user vimrc file: "~/.vim/vimrc"
user exrc file: "$HOME/.exrc"
system gvimrc file: "/etc/gvimrc"
user gvimrc file: "$HOME/.gvimrc"
2nd user gvimrc file: "~/.vim/gvimrc"
defaults file: "$VIMRUNTIME/defaults.vim"
system menu file: "$VIMRUNTIME/menu.vim"
fall-back for $VIM: "/usr/share/vim"
Compilation: gcc -c -I. -Iproto -DHAVE_CONFIG_H -DFEAT_GUI_GTK -I/usr/include/gtk-3.0 -I/usr/include/pango-1.0 -I/usr/include/glib-2.0 -I/usr/lib/glib-2.0/inc
lude -I/usr/lib/libffi-3.2.1/include -I/usr/include/fribidi -I/usr/include/harfbuzz -I/usr/include/freetype2 -I/usr/include/libpng16 -I/usr/include/uuid -I/usr
/include/cairo -I/usr/include/pixman-1 -I/usr/include/gdk-pixbuf-2.0 -I/usr/include/libmount -I/usr/include/blkid -I/usr/include/gio-unix-2.0 -I/usr/include/li
bdrm -I/usr/include/atk-1.0 -I/usr/include/at-spi2-atk/2.0 -I/usr/include/at-spi-2.0 -I/usr/include/dbus-1.0 -I/usr/lib/dbus-1.0/include -pthread -D_FORTIFY_S
OURCE=2 -march=x86-64 -mtune=generic -O2 -pipe -fno-plt -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=1
Linking: gcc -L. -Wl,-O1,--sort-common,--as-needed,-z,relro,-z,now -fstack-protector-strong -rdynamic -Wl,-export-dynamic -Wl,-E -Wl,-rpath,/usr/lib/perl5/5.
28/core_perl/CORE -Wl,-O1,--sort-common,--as-needed,-z,relro,-z,now -L/usr/local/lib -Wl,--as-needed -o vim -lgtk-3 -lgdk-3 -lpangocairo-1.0 -lpango-1.0 -la
tk-1.0 -lcairo-gobject -lcairo -lgdk_pixbuf-2.0 -lgio-2.0 -lgobject-2.0 -lglib-2.0 -lSM -lICE -lXt -lX11 -lXdmcp -lSM -lICE -lm -ltinfo -lelf -lnsl -lacl
-lattr -lgpm -ldl -Wl,-E -Wl,-rpath,/usr/lib/perl5/5.28/core_perl/CORE -Wl,-O1,--sort-common,--as-needed,-z,relro,-z,now -fstack-protector-strong -L/usr/loca
l/lib -L/usr/lib/perl5/5.28/core_perl/CORE -lperl -lpthread -ldl -lm -lcrypt -lutil -lc -L/usr/lib -ltclstub8.6 -ldl -lz -lpthread -lm
```
coq
```
λ › coqtop --version ~ master
The Coq Proof Assistant, version 8.9.0 (January 2019)
compiled on Jan 23 2019 20:02:39 with OCaml 4.07.1
```