coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin
Chronological Thread
- From: Makarius <makarius AT sketis.net>
- To: t x <txrev319 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin
- Date: Mon, 8 Jul 2013 11:35:49 +0200 (CEST)
On Fri, 5 Jul 2013, t x wrote:
What is required to merge these changes into the main Coq branch? I had stumbled across this project earlier, wanted to use it, but did not want to be forced to choose between "being able to use Pide" vs "being able to have new Coq bug fixes / features."
I do not understand the Coq development process, so I can't tell. Maybe some of the French colleagues can explain this (who are also collaborating in a joint project).
Technically, CoqPIDE is doing the main (generic) protocol connectivity, and demonstrates it by some toy protocol functions for CoqIde-style syntax highlighting. This was reasonably easy to do with minor changes on Coq 8.4 sources. Anybody experimenting with further functionality could start by making local patches that are re-adjusted everytime Coq changes, using one of its git clones.
I have seen this technique of following upstream changes systematically in the Eclipse front-end for PIDE, which was done by Andrius Velykis (see also https://github.com/andriusvelykis). Note that is for alternative PIDE front-ends, not prover back-ends.
The basic CoqPIDE connectivity layer merely liberates the prover from old problems of TTY-style communication of plain text via stdin/stdout/stderr, and avoids common mistakes in using XML naively. Substantial work would be required to improve the Coq back-end to support actual document-oriented interaction, as required for a realistic Prover IDE.
I would like to encourage that nonetheless: it greatly helps to open up arcane interactive provers towards a wider audience. (Although users of vi or emacs actually like arcane things.)
Makarius
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, (continued)
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Benjamin Berman, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Carst Tankink, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Boutillier, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Courtieu, 07/08/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Carst Tankink, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Benjamin Berman, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Carst Tankink, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Makarius, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Abhishek Anand, 07/06/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Makarius, 07/08/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
Archive powered by MHonArc 2.6.18.