The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Mar 03, 2014 at 03:24:30PM +0100, Laurent Théry wrote:
> Juste par curiosité, c'est quoi ce "even more are coming"?

What follows is still science fiction, but thigs moves fast...

As part of the Paral-ITP ANR Carst Tankink is currently linking Coq with
the PIDE framework originally developed for Isabelle/Jedit.  This
middleware has Jedit as its primary GUI but also a web based one (and
maybe even an Eclipse one).  These user interfaces are conceptually
similar to the ones we have today (a text editor), but will deliver a
better user experience, especially to egineers.

As part of the do-coq Digiteo project François Poulain is working on
a bridge between Coq and TeXmacs, a WYSIWYG mathematical editor.  In
this case the editor is being made aware of Coq's notations and the
current focus is on editing/rendering formulas.  The ascii "\sum_(i | i
< n) F i" we have in MathComp will be rendered on the screen as it
would in a .pdf file generated via pdflatex; texmacs will let you
edit such bi-dimensional formula with your mouse and produce the
corresponding ascii text (in the .v file).

But don't hold your breath, none of that is ready yet ;-)

Ciao
-- 
Enrico Tassi