Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coqtop -ideslave on Mac OS X

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coqtop -ideslave on Mac OS X


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coqtop -ideslave on Mac OS X
  • Date: Tue, 17 Feb 2015 18:27:07 +0100

On Tue, Feb 17, 2015 at 04:57:17PM +0000, Kevin King wrote:
> When I run version 8.5beta1 of coqtop on Mac OS X with -ideslave, I get the
> following debug info:
>
> Would anyone have an idea how to remedy this?

Hello, in Coq 8.5 the protocol between CoqIDE and coqtop changed and
also how coqtop is started. This is an example of the command line
CoqIDE uses:

coqtop -main-channel stdfds -control-channel 127.0.0.1:48310 -ideslave

IIRC the control channel is optional, but you must tell coqtop how to
connect to the UI (main channel), either using a pipe as in the example
or using a socket (as for the control channel, HOST:PORT).

I'll look at the error message and try to make it more informative.

To get more info about the new protocol used by CoqIDE:

coqtop -toploop coqidetop --help-XML-protocol

Last, the main loop of coqtop can now be changed by providing a plugin
in the toploop/ directory. CoqIDE makes no exception (if you install
coq system wide you find coqidetop.cmxs inside this directory).
If you are interested in developing a UI for Coq, this gives you the
freedom to choose the communication protocol you prefer.

There is no documentation, so feel free to ask.

Best,
--
Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page