Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
I installed coq and coqtail in my computer. According to this page:
https://github.com/whonore/Coqtail
Im now supposed to use the command
CoqStart
to launch the plugin. However, when I type ":CoqStart" the system responds: "E492: Not an editor command: CoqStart"
So, what should I do instead?
That error likely means either Coqtail wasn't installed correctly, it didn't load because of the file type, or it doesn't support your version of Vim/NeoVim.
To check for the first case, see if Coqtail is in your Vim runtime path (:echo &rtp). If not, double check that you didn't miss a step while installing with whatever package manager you're using (e.g., forgetting to do :PlugInstall with vim-plug). See https://github.com/whonore/Coqtail#installation-and-requirements for some options.
If it is installed, make sure the buffer you're editing has filetype=coq. This should be set automatically if you open a .v file, but you can also set it manually with :set ft=coq.
Finally, if everything is installed and you're editing a Coq file, check if g:coqtail#supported is 0. Coqtail requires Python 3.6 or newer and it will fail to load and print an error if your Vim/NeoVim installation doesn't have it.
