The Coq mailing list

[Ryan Rusich <rusichr AT cs.ucr.edu>]

Deal All, Thank you for your time and assistance. This was indeed what I was inquiring about.

On Fri, Jun 5, 2009 at 11:50 PM, Yves Bertot <Yves.Bertot AT sophia.inria.fr> wrote:

Ryan Rusich wrote:

Dear All, Can anyone point me in the direction of the documentation for
extracting natural language from proofs using Coq? I read that it was
included in Coq from version 6.2 on, but have run into some difficulty
identifying the name of the command, and the location documentation
pertaining to it on the Coq website.
Thank you,
Ryan

 

If I remember correctly, the support for this command has been discontinued.  The best documentation on this capability is documented in references 87, 95, 102 of http://www-sop.inria.fr/marelle/projet.html (today's version).

We (the Lemme/Marelle team at INRIA Sophia) still have a tool chain that produces natural language text from proofs, but it is external to Coq, and we definitely have a hard time to maintain it.  It is based on the Pcoq system, which is 50% compatible with the newest version of Coq (not all tactics are supported, the module system is not, notations are not, and so on).

The best references on this work are 47, 70, 71, 81, 87, 90, 92, 95, 100, 102, 104, 105.

I always dream of putting this software back on public distribution.  It has some funny capabilities, but it is hard to maintain.  We used it intensively for some of our first big proofs, but we don't anymore: we now use proof-general or coqide.

Yves

-- 
Cheers, Ryan