The Coq mailing list

[Jasper Haag <jasper AT bedrocksystems.com>]

Hello,

My team is interested in creating a central reference manual using Sphinx (or potentially another tool) and then linking this with documentation for the in-house libraries which we've developed. Currently the documentation for our libraries is generated using coqdoc, but it is unclear to me how I should effectively cross-reference this from within our Sphinx manual. In particular, Sphinx has nice support for cross-references using sphinx.ext.intersphinx, but both sets of documentation must be created using Sphinx in order for that to work.

Have folks dealt with integrating coqdoc with Sphinx (or other documentation tools) in the past? Ideally I would be able to use (or create) a small tool which massages the output from coqdoc into something that Sphinx can ingest; besides easy cross-referencing, keeping a consistent interface is nice. Another idea I had was to parse the index (or TOC) from coqdoc and then inject that into the Sphinx build process in order to resolve identifier references. Are there better ways to accomplish this cross-referencing?

Thanks!

Jasper Haag - Formal Methods Engineer

BedRock Systems, Inc.