Running vim without filename: E492: Not an editor command: CoqStart

[hyperpenelope]

If I start Vim without opening a particular file (i.e. just running vim), I cannot use Coqtail commands. For example, if I execute :CoqStart. I get the error E492: Not an editor command: CoqStart. However, if I run vim coqfile.v,, then the Coqtail commands are available and I can use this cool package. It does not matter whether coqfile.v already exists or not - Coqtail works in either case.

Obviously, I have a straightforward workaround - always give a file name to Vim when I want to use Coqtail. However, I did spend at least an hour in frustration before stumbling upon this, so I do think it counts as a (minor) bug.

Note: when I open Vim without specifying a file name, I can see that Coqtail has been loaded by running :scriptnames:

:scriptnames
  1: /etc/vim/vimrc
  2: /usr/share/vim/vim90/debian.vim
  3: ~/.vimrc
  4: /usr/share/vim/vim90/syntax/syntax.vim
--- snip ---
 23: /usr/share/vim/vim90/plugin/zipPlugin.vim
 24: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail/channel.vim
 25: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail/compat.vim
 26: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail/coqproject.vim
 27: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail/panels.vim
 28: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail/util.vim
 29: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail/version.vim
 30: ~/.vim/pack/coq/start/Coqtail/autoload/coqtail.vim
 31: ~/.vim/pack/coq/start/Coqtail/ftdetect/coq.vim
 32: /usr/share/vim/vim90/syntax/help.vim
 33: /usr/share/vim/vim90/ftplugin/help.vim

Version info

$ coqtop --version
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.13.1
$ vim --version
VIM - Vi IMproved 9.0 (2022 Jun 28, compiled May 04 2023 10:24:44)
Included patches: 1-1378, 1499
Modified by team+vim@tracker.debian.org
Compiled by team+vim@tracker.debian.org
Huge version with GTK3 GUI.  Features included (+) or not (-):
+acl               +file_in_path      +mouse_urxvt       -tag_any_white
+arabic            +find_in_path      +mouse_xterm       +tcl
+autocmd           +float             +multi_byte        +termguicolors
+autochdir         +folding           +multi_lang        +terminal
-autoservername    -footer            -mzscheme          +terminfo
+balloon_eval      +fork()            +netbeans_intg     +termresponse
+balloon_eval_term +gettext           +num64             +textobjects
+browse            -hangul_input      +packages          +textprop
++builtin_terms    +iconv             +path_extra        +timers
+byte_offset       +insert_expand     +perl              +title
+channel           +ipv6              +persistent_undo   +toolbar
+cindent           +job               +popupwin          +user_commands
+clientserver      +jumplist          +postscript        +vartabs
+clipboard         +keymap            +printer           +vertsplit
+cmdline_compl     +lambda            +profile           +vim9script
+cmdline_hist      +langmap           -python            +viminfo
+cmdline_info      +libcall           +python3           +virtualedit
+comments          +linebreak         +quickfix          +visual
+conceal           +lispindent        +reltime           +visualextra
+cryptv            +listcmds          +rightleft         +vreplace
+cscope            +localmap          +ruby              +wildignore
+cursorbind        +lua               +scrollbind        +wildmenu
+cursorshape       +menu              +signs             +windows
+dialog_con_gui    +mksession         +smartindent       +writebackup
+diff              +modify_fname      +sodium            +X11
+digraphs          +mouse             +sound             -xfontset
+dnd               +mouseshape        +spell             +xim
-ebcdic            +mouse_dec         +startuptime       -xpm
+emacs_tags        +mouse_gpm         +statusline        +xsmp_interact
+eval              -mouse_jsbterm     -sun_workshop      +xterm_clipboard
+ex_extra          +mouse_netterm     +syntax            -xterm_save
+extra_search      +mouse_sgr         +tag_binary        
-farsi             -mouse_sysmouse    -tag_old_static    
   system vimrc file: "/etc/vim/vimrc"
     user vimrc file: "$HOME/.vimrc"
 2nd user vimrc file: "~/.vim/vimrc"
      user exrc file: "$HOME/.exrc"
  system gvimrc file: "/etc/vim/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"

[whonore]

Thanks for reporting, but I believe this is working as intended. Coqtail uses Vim's autoload and ftplugin features to avoid registering commands, mappings, functions, etc. for non-Coq files. Whether a buffer is considered to be a Coq file is determined by its filetype. This is set automatically for paths that end in .v, but nameless buffers have an empty filetype by default.

You can set the filetype manually with :setfiletype coq. Or, if you want to treat nameless buffers as Coq by default, I think putting setfiletype FALLBACK coq in your .vimrc would work, although I haven't really tested that.

[hyperpenelope]

Thank you for the answer. Okay, that makes sense. If I made a pull request which added a sentence about this behaviour to README.md, do you think it would be merged? I would insert something like the following immediately under the section header "Usage":

Once Coqtail has been installed, its commands are available whenever you edit a Coq file (with the .v extension). Alternatively, you can run :setfiletype coq when editing any buffer to tell Vim that you are writing Coq code, which will then make Coqtail's commands available.

[whonore]

Sure, improvements to the documentation are appreciated. I might just edit the wording slightly before merging.

[whonore]

Closed by #365.