The Coq mailing list

[jean-francois.monin AT imag.fr]

Hello,

Here is a third possibility :

http://why.lri.fr/index.en.html

Regards,
  Jean-Francois

Joseph N. Ruskiewicz a ecrit :
 > Hello Everybody:
 >     I am quite new to both OCaml and Coq.  (2 weeks).
 > 
 >     I am enjoying both of them immensely.
 > 
 >     I would like to implement a formal method front end that will 
 > generate the proof obligations and allow the user to prove them using Coq.
 > 
 >     My question is this:  What is the best way to move forward with this?
 > 
 >     I have investigated a few possibilities and have come up with two 
 > that I would like to pursue.
 >    
 >     1.  using coqmktop, which I have been playing with but not having 
 > much luck.  Any pointers?
 > 
 >     2.  Or using the libraries from Coq and writing a specialized front 
 > end.  I would like to do my pre-parsing and then introduce the user with 
 > the usual Coq input/output (coqtop) with the proof obligations.
 > 
 >     Will any of these work?  Or should I pursue a different path?
 > 
 >     Also, is there any word on when Coq'Art will be purchasable?
 > 
 >    Thank you all.
 > 
 > Joseph
 > --------------------------------------------------------
 > 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