Stream: Dune devs & users

Topic: Coqdoc rules for dune


view this post on Zulip Rudi Grinberg (Aug 21 2020 at 22:29):

I'm investigating adding rules for generating documentation pages for coq in dune. We already have a similar functionality for OCaml, and it would be cool to make it work for coq. How do users generate documentation currently? Do coq make files include rules for running coqdoc? If so, are these rules documented somewhere?

view this post on Zulip Ali Caglayan (Aug 21 2020 at 23:15):

I was interested in getting dune to do this for my coq project recently too. All I could find was this: https://github.com/coq/coq/pull/9649

view this post on Zulip Rudi Grinberg (Aug 21 2020 at 23:57):

Thanks. That's a useful reference. It should be simple to setup a rule like that for every coq theory

view this post on Zulip Paolo Giarrusso (Aug 22 2020 at 08:57):

How would you get the glob files? Coq dune doesn't seem to produce them usually...

view this post on Zulip Gaëtan Gilbert (Aug 22 2020 at 09:56):

The missing glob files are just a bug, see eg https://github.com/coq/coq/issues/12699#issuecomment-659056226

view this post on Zulip Paolo Giarrusso (Aug 22 2020 at 14:42):

Okay, but I cannot find an actual relevant issue or a fix version.

view this post on Zulip Paolo Giarrusso (Aug 22 2020 at 14:46):

and I’m fine sticking with coq_makefile for most tasks, next to dune, so no pressure, but building coqdoc with dune still sounds impossible until that’s fixed, and I see no ETA for that fix.

view this post on Zulip Paolo Giarrusso (Aug 22 2020 at 14:47):

but since I don’t get dune, I’m happy to be corrected :-)

view this post on Zulip Rudi Grinberg (Aug 22 2020 at 23:49):

Gaëtan Gilbert said:

The missing glob files are just a bug, see eg https://github.com/coq/coq/issues/12699#issuecomment-659056226

Fixed here I believe https://github.com/ocaml/dune/pull/3721

view this post on Zulip Rudi Grinberg (Aug 22 2020 at 23:50):

Paolo Giarrusso said:

and I’m fine sticking with coq_makefile for most tasks, next to dune, so no pressure, but building coqdoc with dune still sounds impossible until that’s fixed, and I see no ETA for that fix.

You're too pessimistic ;)

view this post on Zulip Rudi Grinberg (Aug 22 2020 at 23:51):

Paolo Giarrusso said:

but since I don’t get dune, I’m happy to be corrected :-)

Happy to address whatever skepticism you may have

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:04):

I'm sorry, there might be two discussions going on.

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:04):

As a dune _user_, my question might be "when does this ship? (but no pressure)".

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:06):

in this case "when does a way to build coqdoc ship"

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:09):

more in general, I guess I wonder if dune builds are ever going to replace other useful features of coq_makefile (including build timings) or (as I currently assume) we should keep supporting coq_makefile indefinitely

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:12):

having said all that, Dune's support for build caching is amazing, and what'd probably be much more important would be a way to combine that with make vos and attain build-time nirvana :-)

view this post on Zulip Rudi Grinberg (Aug 23 2020 at 22:18):

Paolo Giarrusso said:

more in general, I guess I wonder if dune builds are ever going to replace other useful features of coq_makefile (including build timings) or (as I currently assume) we should keep supporting coq_makefile indefinitely

What are build timings?

view this post on Zulip Rudi Grinberg (Aug 23 2020 at 22:19):

Paolo Giarrusso said:

in this case "when does a way to build coqdoc ship"

Maybe 2.8? It doesn't seem like such a difficult feature. The main bottleneck is my lack of understanding of how coqdoc + coq_makefile currently works. For example, does it build and install the documentation by default?

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:54):

https://coq.github.io/doc/v8.12/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile has lots of targets, including https://coq.github.io/doc/v8.12/refman/practical-tools/utilities.html#timing-targets-and-performance-testing, which produce various kinds of information about build timing. I'm not sure how much of that makes sense in dune, honestly.

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:57):

on coqdoc, docs are neither built by default nor ever "installed" AFAIK — people seem to run coqdoc by hand on the output of coq_makefile, and pre- and post-process it in various ways

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 22:58):

hm, scratch "coqdoc by hand"

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 23:01):

and install-html exists, but I have never seen it used.

view this post on Zulip Paolo Giarrusso (Aug 23 2020 at 23:03):

But the point on processing seems to stand, because coqdocjs requires at least adding a couple resources to the output, beyond the coqdoc flags

view this post on Zulip Karl Palmskog (Aug 23 2020 at 23:20):

see here for an example of a coq_makefile enhancement for producing custom call to coqdoc: https://github.com/coq-community/huffman/blob/master/Makefile.coq.local

view this post on Zulip Karl Palmskog (Aug 23 2020 at 23:21):

basically, it's very common to pass special flags to coqdoc to specialize the output and output location

view this post on Zulip Rudi Grinberg (Aug 23 2020 at 23:29):

Paolo Giarrusso said:

https://coq.github.io/doc/v8.12/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile has lots of targets, including https://coq.github.io/doc/v8.12/refman/practical-tools/utilities.html#timing-targets-and-performance-testing, which produce various kinds of information about build timing. I'm not sure how much of that makes sense in dune, honestly.

Build timing still makes sense in dune. Thankfully we already have that covered with --trace-file. It works for OCaml as well

view this post on Zulip Ali Caglayan (Aug 24 2020 at 02:50):

How do you make sense of a trace file?

view this post on Zulip Rudi Grinberg (Aug 24 2020 at 07:05):

Ali Caglayan said:

How do you make sense of a trace file?

You can use chrome. Just open chrome://tracing in the url

view this post on Zulip Paolo Giarrusso (Aug 24 2020 at 08:03):

Rudi Grinberg said:

Build timing still makes sense in dune. Thankfully we already have that covered with --trace-file. It works for OCaml as well

That doesn't cover TIMING=1. Makefiles also include visualization scripts — there's no need to do that job in _dune_, but it should be doable somehow.

view this post on Zulip Paolo Giarrusso (Aug 24 2020 at 08:13):

there are also pretty-timed and print-pretty-timed-diff, but honestly the output of make TIMED=1 is more useful than what I can get in catapult by loading a trace.

view this post on Zulip Paolo Giarrusso (Aug 24 2020 at 08:17):

in any case, that's why I'm not in a hurry to replace coq_makefile by dune — except for the killer feature of build caching :-)

view this post on Zulip Emilio Jesús Gallego Arias (Aug 24 2020 at 09:01):

Timing needs a bit of improvement, in particular for Dune to get some finer data; but IMHO we won't follow the same path that coq_makefile here (parsing some stdout), see some recent PRs.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 24 2020 at 09:02):

coqdoc rules should be quite easy, IIANM to generate Foo.html from Foo.v you just need to pass Foo.{v,glob}, I think coqdoc has problems resolving links so we tend to call it as coqdoc $ALL_VO $ALL_GLOB

view this post on Zulip Emilio Jesús Gallego Arias (Aug 24 2020 at 09:02):

coqdoc should be fixed so it can build incrementally tho

view this post on Zulip Karl Palmskog (Aug 24 2020 at 09:14):

So currently, .glob files are installed by coq_makefile, but are not installed by Dune, even after the PR to add them as targets. I thought local .glob files for other projects could be used by coqdoc? Which is the desired behavior, the one by coq_makefile or Dune? Are there any plans to synchronize the installation behavior?

view this post on Zulip Rudi Grinberg (Aug 24 2020 at 10:01):

@Enrico Tassi seems like .glob files need to be installed after all? if coq_makefile is doing it.

view this post on Zulip Rudi Grinberg (Aug 24 2020 at 10:02):

Emilio Jesús Gallego Arias said:

Timing needs a bit of improvement, in particular for Dune to get some finer data; but IMHO we won't follow the same path that coq_makefile here (parsing some stdout), see some recent PRs.

Indeed. Parsing stdout sounds very yucky. An interesting approach to explore would be to add a library that emits instrumentation information that dune can read.

view this post on Zulip Rudi Grinberg (Aug 24 2020 at 10:03):

Emilio Jesús Gallego Arias said:

coqdoc rules should be quite easy, IIANM to generate Foo.html from Foo.v you just need to pass Foo.{v,glob}, I think coqdoc has problems resolving links so we tend to call it as coqdoc $ALL_VO $ALL_GLOB

In that case, I can take a stab at it.

view this post on Zulip Karl Palmskog (Aug 24 2020 at 10:07):

coqdoc prefixes files with their logical path, so if the top-level logical path is Bar, then the filename for Foo.v becomes Bar.Foo.html. I guess this is needed since there may be conflicting module/file names with different logical paths, and the coqdoc HTML directory structure is flat

view this post on Zulip Enrico Tassi (Aug 24 2020 at 15:53):

Rudi Grinberg said:

Enrico Tassi seems like .glob files need to be installed after all? if coq_makefile is doing it.

I still miss who/which tool is using them, other than coqdoc. I was expecting dune to run coqdoc. Is there any other user?

view this post on Zulip Karl Palmskog (Aug 24 2020 at 16:47):

coq2html uses *.glob files as well, but that's not why they are installed for sure

view this post on Zulip Rudi Grinberg (Aug 24 2020 at 17:41):

Say my coq project against building against some installed library and I'd like to build the docs. Do I need the .glob files for the installed library?

view this post on Zulip Li-yao (Aug 24 2020 at 17:52):

you only need FILE.glob to build the docs of FILE.v

view this post on Zulip Karl Palmskog (Aug 24 2020 at 19:50):

many Coq projects don't provide any kind of documentation online to link against (--external option to coqdoc). It may become a common occurrence to produce documentation not only for one's own project, but for all the libraries one uses, and bundle them together. This would only be possible if .glob files are installed for every dependency.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2020 at 09:39):

Li-yao said:

you only need FILE.glob to build the docs of FILE.v

Are you sure about this @Li-yao ? Will coqdoc link the definitions to other files correctly? Indeed I think that if A.v uses B.v, you need to pass B.glob too so A.html knows where to link? I'll try to have a look ASAP, but I may be busy this week

view this post on Zulip Li-yao (Aug 25 2020 at 19:13):

I might be missing something, but I think that for every token to be hyperlinked, you only need the name of the module and an anchor, both of which are given in the current module's .glob file.

view this post on Zulip Ali Caglayan (Sep 01 2020 at 15:46):

@Rudi Grinberg Any progress with this?

view this post on Zulip Rudi Grinberg (Sep 01 2020 at 21:40):

No updates yet. I'd like to have something ready for 2.8 or 2.9 though (1-3 months)


Last updated: Oct 16 2021 at 09:07 UTC