coq 8.9.0 support

[VisualizeTheWorld]

When issuing :CoqLaunch under Coq 8.9.0, vim freezes with the message

Don't know what to do with -ideslave
See -help for the list of supported options

vim does not respond to ^c or ^z after this point, and must be killed.

[splintersuidman]

The changelog for Coq 8.9.0 states:

Coq binaries and process model

• Before 8.9, Coq distributed a single coqtop binary and a set of dynamically loadable plugins that used to take over the main loop for tasks such as IDE language server or parallel proof checking.

  These plugins have been turned into full-fledged binaries so each different process has associated a particular binary now, in particular coqidetop is the CoqIDE language server, and coq{proof,tactic,query}worker are in charge of task-specific and parallel proof checking.

Instead of coqtop -ideslave, coqidetop should be run. The fix is the following diff:

diff --git a/autoload/coqtop.py b/autoload/coqtop.py
index 3a181d0..0dc5733 100644
--- a/autoload/coqtop.py
+++ b/autoload/coqtop.py
@@ -203,8 +203,7 @@ def send_cmd(cmd):
 def restart_coq(*args):
     global coqtop, root_state, state_id
     if coqtop: kill_coqtop()
-    options = [ 'coqtop'
-              , '-ideslave'
+    options = [ 'coqidetop'
               , '-main-channel'
               , 'stdfds'
               , '-async-proofs'

I could open a pull request with this change, but I'm not sure how to deal with backwards-compatibility. (And this repository does not seem to be very active.)

[splintersuidman]

I have created a fork at https://github.com/splintah/coquille. In the mean time, you can use the plugin from there.

[VisualizeTheWorld]

Thanks!

[code-hunger]

I came here from a Google search, maybe it's worth mentioning this in the README.