The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

For the last few years, I've been working on Certified Programming with 
Dependent Types <http://adam.chlipala.net/cpdt/>, a book introducing Coq 
by following a particular pragmatically oriented approach.  A print 
version is slated to appear from MIT Press, and I'm lately drawing 
closer and closer to a version that I'm ready to submit to begin the 
publication process.  The currently posted online version includes all 
content changes that I've had planned; I'll really appreciate any 
bug/typo finding, suggestions, etc., that folks can offer on the latest 
draft!

The main reason I'm writing to coq-club has to do with typesetting.  
coqdoc is really quite convenient for generating nice-looking PDF's via 
LaTeX from Coq code.  However, there are enough warts that the output 
isn't formatted well enough to commit to paper.  I've run into some 
issues with improper font selection, spacing choices that don't look 
very nice, and so on.  Some of these I've worked around by including 
LaTeX code explicitly in the source, but eventually I gave up on that 
and left some parts ugly.  I would like the final version to work 
without any nasty manual LaTeX.

I imagine the required changes to coqdoc wouldn't need too much coding 
work, but I'm not yet familiar with the implementation myself.  Would 
anyone on the Coq team be interested in working with me to fine-tune 
coqdoc?  Here I'm only concerned with LaTeX output, not HTML output.

It would also be nice to see some more convenience forms for indicating 
formatting to be honored in both LaTeX and HTML.  For instance, I 
sometimes want to include links, which can be put in footnotes in LaTeX 
and linked in the normal way in HTML.

Thanks in advance to anyone who can help here!