The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

2012/1/12 Luminous Fennell <mstrlu AT gmx.net>

On Thu, Jan 12 2012 at 17:06 +0100, Adam Chlipala wrote:

> Luminous Fennell wrote:
>> Over the holidays, I wrote some Haskell code to export Coq definitions
>> to LaTeX or ASCII documents.[...]
>>
>> My questions is, if it would be worth it to put a little bit more effort
>> in this (i.e. making a real project out of this). Is there already such
>> a tool? And if not would anybody else be interested or find this useful?
>>
>
> Have you looked at coqdoc, which is included in the standard Coq
> distribution?  It has been used successfully to typeset several books.
> (It only covers LaTeX and HTML, not ASCII.)

Well, coqdoc is more a tool for code documentation; it's great for
exporting the actual source code, but I would be more interested in
exporting the definitions in a more informal form, like you would write
them in an email or paper. So instead of

has_type : env -> exp -> ty -> Prop =
...
| ht_app : forall e f E t1 t2,    has_type E e (t1 --> t2)
                              -> has_type E f t1
                              -> has_type E (app e f) t2

the tool should give me something like:

has_type:

ht_app: [ E |- e : t1 --> t2,
         E |- f : t1 ]
       ==>
         E |- e f : t2

Maybe using Coq Notation capabilities + coqdoc will give you what you need..

 

And for the LaTeX version, the output should be close to how I would
typeset it manually in a thesis or paper, so that I can keep a
automatically generated version as long as possible in the draft.

Best regards

Lu

-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.