The Coq mailing list

[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

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