The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

1) You can just run coqdoc twice, right?  Once for html and once for .tex.

2) I believe if you have .vo/.glob/.v.d/whatever files around (i.e., if you've compiled your development with coq_makefile first), then it'll do inter-file links, at least in HTML

3) If I recall correctly, there's an --interpolate option or similar that gets something like this (though I don't think it does inter-file)

4) I have worked around that issue by using an old version of proviola, slightly patched.  It is available at https://github.com/JasonGross/proviola-source (master branch).  It works on the HoTT library, even when I pass coqdoc --utf-8 (or was it --utf8?).  If you patch it further to make it handle your code, I'm happy to accept pull requests to my fork, while waiting for the author of the tool to fix the newer version.  The setup we use for HoTT is ... um ... well, not quite, but almost, documented, at https://github.com/HoTT/HoTT/blob/master/.travis.yml and https://github.com/HoTT/HoTT/blob/master/etc/ci/generate_and_push_doc.sh.

Note that proviola also can't handle (* begin hide *).

I think you don't need the dev version for any of these, but I'm not sure; I've been using them mostly for HoTT, which used trunk as-of mid-summer or so.

-Jason

On Tue, Feb 11, 2014 at 9:25 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Hi,
I could not yet find tool(s) to export our coq development which spans multiple files in a way that satisfies the following requirements:
1) I need both HTML and .tex outputs
2) Coq identifiers  should be hyperlinked to their definition. AFAIK, coqdoc only does this if the definition(lemma/fixpoint/inductive/notation) is in the current file.
The idea is that if the resultant .tex files are included in a larger .tex document, hyperlinks across these .tex files should work. The same should be true if the generated HTML files are uploaded to the web in the same folder.

3) Occurrences of coq identifiers in comments (** *) must also be hyperlinked and colored appropriately.

4) There should be a Proviola mode for HTML. I have had many issues in using the current Proviola tool (e.g. https://bitbucket.org/Carst/proviola-source/issue/18/proviola-python-273-barfs-on-some-unicode) .

5) There should be a coqdoc command/marker that gets replaced by the proof state at the position wherever it occurs.

Please let me know if there is already a collection of tools that can satisfy the above requirements. Also, does the development version of coqdoc already achieve 2) and 3) ?

If there is no such collection of tools, I plan to write a single (open source) command line tool that does all the above. I plan to reuse the infrastructure that I already built for my netbeans-coq plugin. I welcome suggestions on how to extend the above list of requirements so that this tool would be useful for others as well. For 2) and 3), I still don't know a good way to handle the case when the target definition is hidden using the (* begin hide *) mechanism.

Thanks,
Abhishek