The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Hoi Carst,

Ik heb geprobeerd het te installeren, maar zit op het moment vast op
een niet compilerende Coq:
http://coq-bench.github.io/

Heb jij een precieze versie die werkt?

On Wed, Nov 26, 2014 at 4:51 PM, Carst Tankink 
<carst.tankink AT inria.fr>
 wrote:
> It is with great pleasure that I announce the first public testing release
> of Coq/jEdit (version 0.1.1): an asynchronous editing environment for Coq
> proofs.
> The release can be downloaded from
>
> http://pages.saclay.inria.fr/carst.tankink/jedit.html
>
> This page also contains installation and usage instructions. The most import
> requirement is that the editor relies on several improvements to be
> introduced in Coq 8.5, and therefore only works with certain changesets of
> Coq-trunk as a lower bound.
>
> This is a beta/testing release, so do not hesitate to contact me if there
> are any issues in installation or usage.
>
>
> More information about the editor follows:
>
> * What is an asynchronous editing environment?
> In this editing model, you 'just' type your proof: the proof assistant is
> always on, and continuously provides feedback on your proof. This is similar
> to a spell checker in a word processor, or the highlighting of compilation
> errors in Eclipse: commands that failed to apply are underlined in red as
> you type, and you are free to edit the text wherever you want.
>
> Of course, it is still possible to inspect the goalstates or error messages,
> by putting the text cursor on the lines of the  command you want to see the
> output of. This is displayed in a contextual panel, that updates as you move
> through the text, so you do not have to go into Proof General mode and
> (un)lock a region every time you want to inspect a state.
>
> * Any other features?
> You can Ctrl+click on lemmas and theorems to open the file they are defined
> in, and jump directly to the definition.
>
> You can execute queries in a separate contextual panel.
>
> It has syntax highlighting, statically for now, but we plan to add
> prover-driven syntax highlighting in a future release.
>
> The plugin builds on a generic (Scala) library called PIDE, so if you want
> to process Coq proofs in your own project, you can use the PIDE
> datastructures and functions, instead of having to hand-roll your own XML
> processing functions and doing low-level interaction with the prover.
>
>
> * What is jEdit?
> jEdit is a generic (programming) text editor that can be extended by
> plugins. Coq/jEdit is one such plugin.
>
> * Who's responsible?
> The tool was developed as part of the ANR Paral-ITP project
> (http://paral-itp.lri.fr/). The original editor plugin was written for
> Isabelle by Makarius Wenzel. Enrico Tassi developed the parallel computation
> engine for Coq. Finally, Carst Tankink provided the connection between Coq
> and the editor, by generalizing the PIDE library and adding the necessary
> reactions to Coq.
>
>
> Carst Tankink