CoqStart fails because of invalid identifier

[sc8ing]

Running :CoqStart gives the error "Error: Invalid character ':' at beginning of identifier ":".". Afterwards, running any coquille command just prints a full screen of "Coq is already running.". No new panels are opened.

[whonore]

Could you confirm that there aren't any other plugins (like Coquille) that might be interfering?

[sc8ing]

Coquille is not running to the best of my knowledge. I had installed it in the past, but double checked just now to make sure it's not in .vimrc and re-ran :PluginClean.

[whonore]

Could you post the output of :scriptnames after opening a .v file so I can see what files are being sourced?

[sc8ing]

Sure, here is the full output:

  1: ~/.vimrc
  2: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/ftoff.vim
  3: ~/.vim/bundle/Vundle.vim/autoload/vundle.vim
  4: ~/.vim/bundle/Vundle.vim/autoload/vundle/config.vim
  5: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/filetype.vim
  6: ~/.vim/bundle/vim-javascript/ftdetect/javascript.vim
  7: ~/.vim/bundle/tern_for_vim/ftdetect/tern.vim
  8: ~/.vim/bundle/vim-jsx/ftdetect/javascript.vim
  9: ~/.vim/bundle/vim-solidity/ftdetect/solidity.vim
 10: ~/.vim/bundle/vim-fugitive/ftdetect/fugitive.vim
 11: ~/.vim/bundle/vim-clojure-static/ftdetect/clojure.vim
 12: ~/.vim/bundle/coqtail/ftdetect/coq.vim
 13: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/ftplugin.vim
 14: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/indent.vim
 15: ~/.vim/bundle/snow/colors/snow.vim
 16: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/syntax/syntax.vim
 17: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/syntax/synload.vim
 18: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/syntax/syncolor.vim
 19: ~/.vim/plugin/eclim.vim
 20: ~/.vim/eclim/autoload/eclim.vim
 21: ~/.vim/eclim/plugin/eclim.vim
 22: ~/.vim/eclim/autoload/eclim/util.vim
 23: ~/.vim/eclim/autoload/eclim/common/buffers.vim
 24: ~/.vim/eclim/plugin/ftdetect.vim
 25: ~/.vim/eclim/plugin/ftdetect_jdt.vim
 26: ~/.vim/eclim/plugin/java_tools.vim
 27: ~/.vim/eclim/plugin/project.vim
 28: ~/.vim/eclim/plugin/settings_java.vim
 29: ~/.vim/eclim/plugin/vimplugin.vim
 30: ~/.vim/bundle/ale/plugin/ale.vim
 31: ~/.vim/bundle/ale/autoload/ale/events.vim
 32: ~/.vim/bundle/nerdtree/plugin/NERD_tree.vim
 33: ~/.vim/bundle/nerdtree/autoload/nerdtree.vim
 34: ~/.vim/bundle/nerdtree/lib/nerdtree/path.vim
 35: ~/.vim/bundle/nerdtree/lib/nerdtree/menu_controller.vim
 36: ~/.vim/bundle/nerdtree/lib/nerdtree/menu_item.vim
 37: ~/.vim/bundle/nerdtree/lib/nerdtree/key_map.vim
 38: ~/.vim/bundle/nerdtree/lib/nerdtree/bookmark.vim
 39: ~/.vim/bundle/nerdtree/lib/nerdtree/tree_file_node.vim
 40: ~/.vim/bundle/nerdtree/lib/nerdtree/tree_dir_node.vim
 41: ~/.vim/bundle/nerdtree/lib/nerdtree/opener.vim
 42: ~/.vim/bundle/nerdtree/lib/nerdtree/creator.vim
 43: ~/.vim/bundle/nerdtree/lib/nerdtree/flag_set.vim
 44: ~/.vim/bundle/nerdtree/lib/nerdtree/nerdtree.vim
 45: ~/.vim/bundle/nerdtree/lib/nerdtree/ui.vim
 46: ~/.vim/bundle/nerdtree/lib/nerdtree/event.vim
 47: ~/.vim/bundle/nerdtree/lib/nerdtree/notifier.vim
 48: ~/.vim/bundle/nerdtree/autoload/nerdtree/ui_glue.vim
 49: ~/.vim/bundle/nerdtree/nerdtree_plugin/exec_menuitem.vim
 50: ~/.vim/bundle/nerdtree/nerdtree_plugin/fs_menu.vim
 51: ~/.vim/bundle/nerdtree/nerdtree_plugin/vcs.vim
 52: ~/.vim/bundle/vim-airline/plugin/airline.vim
 53: ~/.vim/bundle/vim-airline/autoload/airline/init.vim
 54: ~/.vim/bundle/vim-airline/autoload/airline/parts.vim
 55: ~/.vim/bundle/vim-airline/autoload/airline/util.vim
 56: ~/.vim/bundle/vim-airline-themes/plugin/airline-themes.vim
 57: ~/.vim/bundle/vim-fugitive/plugin/fugitive.vim
 58: ~/.vim/bundle/tagbar/plugin/tagbar.vim
 59: ~/.vim/bundle/vim-fireplace/plugin/fireplace.vim
 60: ~/.vim/bundle/vim-classpath/plugin/classpath.vim
 61: ~/.vim/bundle/vim-clojure-highlight/plugin/vim_clojure_highlight.vim
 62: ~/.vim/bundle/paredit.vim/plugin/paredit.vim
 63: ~/.vim/bundle/rainbow_parentheses.vim/plugin/rainbow_parentheses.vim
 64: ~/.vim/bundle/vim-slime/plugin/slime.vim
 65: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/getscriptPlugin.vim
 66: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/gzip.vim
 67: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/logiPat.vim
 68: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/manpager.vim
 69: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/matchparen.vim
 70: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/netrwPlugin.vim
 71: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/rrhelper.vim
 72: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/spellfile.vim
 73: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/tarPlugin.vim 
 74: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/tohtml.vim
 75: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/vimballPlugin.vim
 76: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/plugin/zipPlugin.vim
 77: ~/.opam/system/share/merlin/vim/plugin/merlin.vim
 78: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/ftplugin/verilog.vim
 79: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/indent/verilog.vim
 80: /usr/local/Cellar/vim/8.1.0800/share/vim/vim81/syntax/verilog.vim
 81: ~/.vim/bundle/vim-airline/autoload/airline/extensions.vim
 82: ~/.vim/bundle/vim-airline/autoload/airline/extensions/quickfix.vim
 83: ~/.vim/bundle/vim-airline/autoload/airline.vim
 84: ~/.vim/bundle/vim-airline/autoload/airline/extensions/netrw.vim
 85: ~/.vim/bundle/vim-airline/autoload/airline/extensions/term.vim
 86: ~/.vim/bundle/vim-airline/autoload/airline/extensions/tagbar.vim
 87: ~/.vim/bundle/vim-airline/autoload/airline/extensions/branch.vim
 88: ~/.vim/bundle/vim-airline/autoload/airline/extensions/fugitiveline.vim
 89: ~/.vim/bundle/vim-airline/autoload/airline/extensions/eclim.vim
 90: ~/.vim/bundle/vim-airline/autoload/airline/extensions/ale.vim
 91: ~/.vim/bundle/vim-airline/autoload/airline/extensions/whitespace.vim
 92: ~/.vim/bundle/vim-airline/autoload/airline/extensions/po.vim
 93: ~/.vim/bundle/vim-airline/autoload/airline/extensions/wordcount.vim
 94: ~/.vim/bundle/vim-airline/autoload/airline/extensions/keymap.vim
 95: ~/.vim/bundle/vim-airline/autoload/airline/section.vim
 96: ~/.vim/bundle/vim-airline/autoload/airline/highlighter.vim
 97: ~/.vim/bundle/vim-airline/autoload/airline/themes/dark.vim
 98: ~/.vim/bundle/vim-airline/autoload/airline/themes.vim
 99: ~/.vim/bundle/vim-airline/autoload/airline/builder.vim
100: ~/.vim/bundle/vim-airline/autoload/airline/extensions/default.vim
101: ~/.vim/bundle/coqtail/ftplugin/coq.vim
102: ~/.vim/bundle/coqtail/autoload/coqtail.vim
103: ~/.vim/bundle/vimbufsync/autoload/vimbufsync.vim
104: ~/.vim/bundle/coqtail/indent/coq.vim
105: ~/.vim/bundle/coqtail/syntax/coq.vim
106: ~/.vim/eclim/autoload/eclim/display/signs.vim
107: ~/.vim/bundle/ale/autoload/ale.vim
108: ~/.vim/bundle/ale/autoload/ale/util.vim
109: ~/.vim/bundle/ale/autoload/ale/linter.vim
110: ~/.vim/bundle/rainbow_parentheses.vim/autoload/rainbow_parentheses.vim
111: ~/.vim/bundle/vim-airline/autoload/airline/async.vim
112: ~/.vim/bundle/tagbar/autoload/tagbar.vim
113: ~/.vim/bundle/tagbar/autoload/tagbar/debug.vim
114: ~/.vim/bundle/tagbar/autoload/tagbar/types/ctags.vim
115: ~/.vim/bundle/tagbar/autoload/tagbar/prototypes/typeinfo.vim
116: ~/.vim/bundle/ale/autoload/ale/engine.vim
117: ~/.vim/bundle/ale/autoload/ale/statusline.vim

[whonore]

Is there any more to the error message? A line number or error code?

[sc8ing]

The only other thing is when scrolling to the bottom of the "Coq is already running." lines that are shown above is says

Error detected while processing function coqtail#Start:
line    1:
E169: Command too recursive
Press ENTER or type command to continue

[whonore]

Ok, I figured out how to reproduce what you're seeing. The initial error message is from Coq if you have something like -Q . :a in _CoqProject. Then the infinite loop of error messages is due to an issue with how I'm registering commands that I'll work on.

[sc8ing]

The same error persists even after updating the plugin to include that commit.

[whonore]

The same error meaning the "Error: invalid character" part or the infinite "Coq is always running"?

[sc8ing]

My bad, that was ambiguous. The invalid character error is the only one that seems to happen now.

[whonore]

Do you have a _CoqProject file?

[sc8ing]

Yes, the contents are -Q . LF.

[whonore]

Could you try adding print(coq_path, *args) in python/coqtail.py on line 133 and show me the output when you do :CoqStart?

[whonore]

And have you checked whether you get this error when using CoqIDE?

[sc8ing]

The output for that is -Q /Users/jacob/Sync/school/pl : thesis/books/software foundations/v1 logical foundations/english/ LF.

I have. There's no problems when using the IDE.

[whonore]

Oh ok, so I think the problem is when . is expanded the spaces aren't getting escaped so Coq thinks you're mapping /Users/... to : and complains that : isn't a valid identifier. CoqIDE seems to handle this correctly when it expands paths, but from some quick checks it seems to fail with an error if you write a path with spaces directly in the _CoqProject file. I'd be curious if you replaced . with the full path in your _CoqProject if you also get an error in CoqIDE.

[whonore]

I pushed a potential fix to coq-proj-escape.

[sc8ing]

That worked! Yes, CoqIDE did give an error when the full path was substituted for the .. Surrounding it with quotes still worked though. Thank you for the fix.

[whonore]

Great, glad we figured it out. I'll add a little more to better handle spaces in paths and merge it probably later this week.