The Coq mailing list

[David Aspinall <David.Aspinall AT ed.ac.uk>]

One possibility would be to look at using PGIP with Coq.  PGIP is 
XML-based protocol for conducting interactive proof.  It is being used 
now to develop the next version of Proof General which will have 
graphical front ends as well as Emacs.  In particular, there is a front 
end based on Eclipse in development.  (Then it would be possible to 
provide plugins for Eclipse which provide graphical editing facilities, 
written in Java of course).

For more details see:  http://proofgeneral.inf.ed.ac.uk/kit

At the moment there is no support for PGIP in Coq, but I believe it 
would be fairly straightforward for someone familiar with the Coq source 
to add.  If anyone is interested in doing this, please drop me a line!

 - David.


Houda Anoun wrote:
> Hi everybody,
> I'm realising a tool using coq as a proof assistant.. till now this tool 
> can't be used by non specialist users ...
> I want to develop a simpl interface using Java but I do not know how to 
> establish the communication between Java and Coq....
> Can anyone give me some ideas about this?
> Thanks a lot
> Houda
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club