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.)

coq 8.9.0 support #75

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions