Stream: Dune devs & users

Topic: Coqdoc rules for dune

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?

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

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

Paolo Giarrusso (Aug 22 2020 at 08:57):

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

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

Paolo Giarrusso (Aug 22 2020 at 14:42):

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

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.

Paolo Giarrusso (Aug 22 2020 at 14:47):

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

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

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 ;)

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

Paolo Giarrusso (Aug 23 2020 at 22:04):

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

Paolo Giarrusso (Aug 23 2020 at 22:04):

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

Paolo Giarrusso (Aug 23 2020 at 22:06):

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

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

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 :-)

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?

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?

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.

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

Paolo Giarrusso (Aug 23 2020 at 22:58):

hm, scratch "coqdoc by hand"

Paolo Giarrusso (Aug 23 2020 at 23:01):

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

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

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

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

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

Ali Caglayan (Aug 24 2020 at 02:50):

How do you make sense of a trace file?

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

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.

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.

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 :-)

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.

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

Emilio Jesús Gallego Arias (Aug 24 2020 at 09:02):

coqdoc should be fixed so it can build incrementally tho

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?

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.

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.

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.

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

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?

Karl Palmskog (Aug 24 2020 at 16:47):

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

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?

Li-yao (Aug 24 2020 at 17:52):

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

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.

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

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.

Ali Caglayan (Sep 01 2020 at 15:46):

@Rudi Grinberg Any progress with this?

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)

Rudi Grinberg (Oct 25 2021 at 18:35):

Some good news: A feature that is required for robust coqdoc rules is being worked on https://github.com/ocaml/dune/pull/5025

Théo Zimmermann (Oct 26 2021 at 08:42):

This is terrific and will not only help with coqdoc but also with making it possible to install the refman of Coq with Dune.

Rudi Grinberg (Oct 26 2021 at 18:11):

Théo Zimmermann said:

This is terrific and will not only help with coqdoc but also with making it possible to install the refman of Coq with Dune.

Hmm, this feature in particular might need extra work. Currently, we have this limitation on the set of installed targets - it must be known without executing any rules. The limitation itself is a left over from dune's more static days, so I think we should be able to lift it.

Théo Zimmermann (Oct 26 2021 at 18:17):

Do you mean that target directories won't be supported for installation even after this PR?

Rudi Grinberg (Oct 26 2021 at 18:42):

Yes. Those need special handling. First of all, I don't even think opam supports them. We need to traverse the directory and flatten it into a list of files to generate the .install file

Emilio Jesús Gallego Arias (Oct 26 2021 at 19:01):

Opam doesn't support them indeed

Emilio Jesús Gallego Arias (Oct 26 2021 at 19:02):

at least not opam 2.0

Last updated: Jun 03 2023 at 18:01 UTC