`:call CoqLaunch()` gives error
Environment
-
coqtop -v
:
The Coq Proof Assistant, version 8.9.1 (August 2019)
compiled on Aug 17 2019 16:43:13 with OCaml 4.02.3
-
nvim -v
:
NVIM v0.4.0-1730-ge2ccf47b5
Build type: Debug
LuaJIT 2.0.5
Compilation: /usr/bin/cc -g -Wall -Wextra -pedantic -Wno-unused-parameter -Wstrict-prototypes -std=gnu99 -Wshadow -Wconversion -Wmissing-prototypes -Wvla -fstack-protector-strong -fdiagnostics-color=always -DINCLUDE_GENERATED_DECLARATIONS -D_GNU_SOURCE -DNVIM_MSGPACK_HAS_FLOAT32 -DNVIM_UNIBI_HAS_VAR_FROM -I/home/username/Downloads/neovim/build/config -I/home/username/Downloads/neovim/src -I/home/username/Downloads/neovim/.deps/usr/include -I/usr/include -I/home/username/Downloads/neovim/build/src/nvim/auto -I/home/username/Downloads/neovim/build/include
Compiled by username@machinename
Features: +acl +iconv +tui
See ":help feature-compile"
system vimrc file: "$VIM/sysinit.vim"
fall-back for $VIM: "/home/username/local/neovim/share/nvim"
Run :checkhealth for more info
-
git log -1
:
commit f9ceda022cd639ae1304f2654be334036445f7d2
Author: LEPILLER Julien <julien.lepiller@irisa.fr>
Date: Fri Jun 28 15:44:00 2019 +0200
- I have run
:UpdateRemotePlugins
in neovim but it didn't help:
Yes, does not help.
Description
Calling :call CoqLaunch()
gives the following error:
line 1:
error caught in request handler '/home/username/.local/share/nvim/site/pack/plugin/start/coquille/rplugin/python3/pycoqtop:function:CoqLaunch [[]]':
Traceback (most recent call last):
File "/home/username/.local/share/nvim/site/pack/plugin/start/coquille/rplugin/python3/pycoqtop/__init__.py", line 68, in launch
self.vim.call('coquille#ShowPanels')
File "/home/username/.local/lib/python3.5/site-packages/pynvim/api/nvim.py", line 299, in call
return self.request('nvim_call_function', name, args, **kwargs)
File "/home/username/.local/lib/python3.5/site-packages/pynvim/api/nvim.py", line 182, in request
res = self._session.request(name, *args, **kwargs)
File "/home/username/.local/lib/python3.5/site-packages/pynvim/msgpack_rpc/session.py", line 102, in request
raise self.error_wrapper(err)
pynvim.api.nvim.NvimError: b'Vim(file):E172: Only one file name allowed: file Goals b17ba966-7291-411e-9e02-13e0932912da'