search

whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
271 stars 35 forks source link

Error on some large operations #351

Closed bn-peters closed 5 months ago

bn-peters commented 5 months ago

Some operations with particularly large outputs currently cause an error:

Error detected while processing function <SNR>68_chanrecv[30]..function <SNR>68_chanrecv:
line    9:
E1510: Value too large:
Press ENTER or type command to continue

Two simple examples that cause this:

Search Prop.

Lemma t (a b c d e f g h i j k : bool) : True.
Proof.
  destruct a, b, c, d, e, f, g, h, i, j, k.
Abort.

This issue might have also locked up my CoqTail (and, by extension, my Vim) instance; although I am not able to reproduce that.

whonore commented 5 months ago

What version of vim/neovim are you using? I'm not able to reproduce that error with your examples on vim 9.0.2190, 9.1.346 or neovim 0.9.5.

bn-peters commented 5 months ago

Good point, I probably should have investigated this further... I can reproduce this with the current Neovim master on MacOS; more specifically this commit. 

$ nvim --version
NVIM v0.10.0-dev-2947+ge1ca7a7bf
Build type: RelWithDebInfo
LuaJIT 2.1.1710088188
Run "nvim -V1 -v" for more info

Also, a perhaps more direct way to reproduce:

Goal True.
Proof.
  do 4000 idtac "Hello World".
Abort.
tomtomjhj commented 5 months ago

backtrace

#0  format_overflow_error (pstart=0x902bdd "*s") at /home/user/neovim/src/nvim/strings.c:999
#1  0x0000000000761171 in vim_vsnprintf_typval (str=0xa32740 <errbuf> "E474: Expected string end:  function getbufvar", str_m=1025, fmt=0x902bc0 "E474: Expected string end: %.*s", ap_start=0x7fffffffb370, tvs=0x0) at /home/user/neovim/src/nvim/strings.c:1623
#2  0x000000000075f318 in vim_vsnprintf (str=0xa32740 <errbuf> "E474: Expected string end:  function getbufvar", str_m=1025, fmt=0x902bc0 "E474: Expected string end: %.*s", ap=0x7fffffffb370) at /home/user/neovim/src/nvim/strings.c:771
#3  0x000000000065b1b8 in semsgv (fmt=0x902bc0 "E474: Expected string end: %.*s", ap=0x7fffffffb370) at /home/user/neovim/src/nvim/message.c:820
#4  0x000000000065b03e in semsg (fmt=0x902bc0 "E474: Expected string end: %.*s") at /home/user/neovim/src/nvim/message.c:785
#5  0x000000000053be78 in parse_json_string (didcolon=<optimized out>, didcomma=<optimized out>, next_map_special=<optimized out>, container_stack=<optimized out>, stack=<optimized out>, pp=<optimized out>, buf_len=32768, buf=0xf76670 "[\"call\", \"coqtail#panels#refresh\", [1, {\"checked\": \"\\\\%1l\\\\|\\\\%>1l\\\\%<3l\\\\|\\\\%3l\\\\%<31c\", \"sent\": null, \"error\": null, \"omitted\": null}, {\"info\": [[\"Hello World\", \"\", \"Hello World\", \"\", \"Hello World\","...) at /home/user/neovim/src/nvim/eval/decode.c:402
#6  json_decode_string (buf=0xf76670 "[\"call\", \"coqtail#panels#refresh\", [1, {\"checked\": \"\\\\%1l\\\\|\\\\%>1l\\\\%<3l\\\\|\\\\%3l\\\\%<31c\", \"sent\": null, \"error\": null, \"omitted\": null}, {\"info\": [[\"Hello World\", \"\", \"Hello World\", \"\", \"Hello World\","..., buf_len=32768, rettv=0x7fffffffc0e0) at /home/user/neovim/src/nvim/eval/decode.c:796
#7  0x000000000055859b in f_json_decode (argvars=0x7fffffffb9a0, rettv=0x7fffffffc0e0, fptr=...) at /home/user/neovim/src/nvim/eval/funcs.c:4510
#8  0x000000000054d25f in call_internal_func (fname=0xf61dd0 "json_decode", argcount=1, argvars=0x7fffffffb9a0, rettv=0x7fffffffc0e0) at /home/user/neovim/src/nvim/eval/funcs.c:291
#9  0x000000000057486a in call_func (funcname=0xf5df30 "json_decode", len=11, rettv=0x7fffffffc0e0, argcount_in=1, argvars_in=0x7fffffffb9a0, funcexe=0x7fffffffbb60) at /home/user/neovim/src/nvim/eval/userfunc.c:1709
#10 0x0000000000571a2f in get_func_tv (name=0xf5df30 "json_decode", len=11, rettv=0x7fffffffc0e0, arg=0x7fffffffc048, evalarg=0x7fffffffc0f0, funcexe=0x7fffffffbb60) at /home/user/neovim/src/nvim/eval/userfunc.c:557
#11 0x0000000000527762 in eval_func (arg=0x7fffffffc048, evalarg=0x7fffffffc0f0, name=0xf62644 "json_decode(l:reply)", name_len=11, rettv=0x7fffffffc0e0, flags=1, basetv=0x0) at /home/user/neovim/src/nvim/eval.c:2315
#12 0x00000000005294dd in eval7 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0, want_string=false) at /home/user/neovim/src/nvim/eval.c:3244
#13 0x0000000000528cde in eval6 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0, want_string=false) at /home/user/neovim/src/nvim/eval.c:2970
#14 0x0000000000528711 in eval5 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0) at /home/user/neovim/src/nvim/eval.c:2825
#15 0x0000000000528223 in eval4 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0) at /home/user/neovim/src/nvim/eval.c:2700
#16 0x0000000000527fdb in eval3 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0) at /home/user/neovim/src/nvim/eval.c:2609
#17 0x0000000000527d97 in eval2 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0) at /home/user/neovim/src/nvim/eval.c:2531
#18 0x0000000000527a5d in eval1 (arg=0x7fffffffc048, rettv=0x7fffffffc0e0, evalarg=0x7fffffffc0f0) at /home/user/neovim/src/nvim/eval.c:2435
#19 0x00000000005278eb in eval0 (arg=0xf62644 "json_decode(l:reply)", rettv=0x7fffffffc0e0, eap=0x7fffffffc200, evalarg=0x7fffffffc0f0) at /home/user/neovim/src/nvim/eval.c:2380
#20 0x000000000057bb5d in ex_let (eap=0x7fffffffc200) at /home/user/neovim/src/nvim/eval/vars.c:449
#21 0x0000000000599015 in execute_cmd0 (retv=0x7fffffffc1b8, eap=0x7fffffffc200, errormsg=0x7fffffffc1d0, preview=false) at /home/user/neovim/src/nvim/ex_docmd.c:1706
#22 0x000000000059afa7 in do_one_cmd (cmdlinep=0x7fffffffc420, flags=7, cstack=0x7fffffffc530, fgetline=0x59772d <get_loop_line>, cookie=0x7fffffffc4d0) at /home/user/neovim/src/nvim/ex_docmd.c:2375
#23 0x00000000005969ec in do_cmdline (cmdline=0x0, fgetline=0x579c04 <get_func_line>, cookie=0xf62b90, flags=7) at /home/user/neovim/src/nvim/ex_docmd.c:665
#24 0x0000000000573468 in call_user_func (fp=0xf1ce70, argcount=3, argvars=0x7fffffffd210, rettv=0x7fffffffd200, firstline=2, lastline=2, selfdict=0x0) at /home/user/neovim/src/nvim/eval/userfunc.c:1188
#25 0x0000000000573bc6 in call_user_func_check (fp=0xf1ce70, argcount=3, argvars=0x7fffffffd210, rettv=0x7fffffffd200, funcexe=0x7fffffffd160, selfdict=0x0) at /home/user/neovim/src/nvim/eval/userfunc.c:1342
#26 0x00000000005747f6 in call_func (funcname=0xf1d2e0 "<SNR>132_chanrecv", len=17, rettv=0x7fffffffd200, argcount_in=3, argvars_in=0x7fffffffd210, funcexe=0x7fffffffd160) at /home/user/neovim/src/nvim/eval/userfunc.c:1700
#27 0x0000000000530a93 in callback_call (callback=0xf1df48, argcount_in=3, argvars_in=0x7fffffffd210, rettv=0x7fffffffd200) at /home/user/neovim/src/nvim/eval.c:6178
#28 0x00000000004e3c4e in channel_callback_call (chan=0xf1d840, reader=0xf1df48) at /home/user/neovim/src/nvim/channel.c:822
#29 0x00000000004e39f2 in channel_reader_callbacks (chan=0xf1d840, reader=0xf1df48) at /home/user/neovim/src/nvim/channel.c:765
#30 0x00000000004e377d in on_channel_event (args=0x7fffffffd368) at /home/user/neovim/src/nvim/channel.c:727
#31 0x00000000007571ae in state_handle_k_event () at /home/user/neovim/src/nvim/state.c:119
#32 0x0000000000681b53 in nv_event (cap=0x7fffffffd500) at /home/user/neovim/src/nvim/normal.c:6586
#33 0x000000000067568b in normal_execute (state=0x7fffffffd490, key=-26365) at /home/user/neovim/src/nvim/normal.c:1229
#34 0x000000000075713e in state_enter (s=0x7fffffffd490) at /home/user/neovim/src/nvim/state.c:101
#35 0x00000000006738b7 in normal_enter (cmdwin=false, noexmode=false) at /home/user/neovim/src/nvim/normal.c:518
#36 0x000000000061989d in main (argc=4, argv=0x7fffffffd868) at /home/user/neovim/src/nvim/main.c:663

There seems to be an error while decoding json (https://github.com/whonore/Coqtail/blob/c881047dd32cbd9524b0c733821c113ebcc03b07/autoload/coqtail/channel.vim#L101, https://github.com/neovim/neovim/blob/e1ca7a7bfc954fae6991fc86d5da1a4eda864903/src/nvim/eval/decode.c#L401-L402), and when reporting the error, the error msg is longer than the limit, so it raises another error before the actual error.

whonore commented 5 months ago

Weird, I'm still not hitting that error with that commit of neovim on MacOS, but thanks to your debugging I think I know what's going on. The first error (E474: Expected string end) is expected. s:chanrecv might only have a partial response so it just tries json_decode, catches the error, and tries again when it gets more data. But it looks like in your case, the partial response is long enough that neovim blows up when it tries to format the error message.

I think I can fix this by actually checking if we have a complete response instead of just blindly trying to decode it. It looks like there should always be an empty string after a complete line so that should be pretty easy to check and I'm not sure why I wasn't doing it to begin with. The only issue would be if neovim also blows up parsing a really long valid JSON string.