The Coq mailing list

["Joseph N. Ruskiewicz" <joseph.ruskiewicz AT inf.ethz.ch>]

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