The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks Jason.

1) yes I can run coqdoc twice. I just listed that as a requirement in the anticipation of knowing about other tools that also satisify the other requirements that coqdoc doesn't. I don't care about getting the latex and html outputs simultaneously.

For 2) and 3), the coqdoc of 8.4pl2 does not seem to work as required. I don't use coq_makefile, but I always run coqc on a file before running coqdoc. And our code does not yet compile with the development version of Coq. If someone can confirm that inter-file hyperlinks work in the latex generated by the new coqdoc, it would be worth the effort to try to make our code compile with the development version of Coq.

4) I had tried your version of Proviola. It certainly eliminated many errors, but not all. Because I'm not so familiar with python, I could not get very far in fixing the remaining issues. I'll try to reproduce the errors and file bug reports.

If there are tools other than coqdoc and Proviola that satisfy many of the 5 requirements listed in my previous email, I'd like to know about them.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Feb 12, 2014 at 8:40 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

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