Stream: Coq users

Topic: Can opam build coqdoc while installing packages?


view this post on Zulip Brandon Moore (May 11 2022 at 14:53):

Is there a convenient way to build the corresponding coqdoc for a coq package installed with opam? (I've tried web searches, but every query has only found results about installing coqdoc itself). Or is using "opam source" and figuring out each package's build instructions the only way?

view this post on Zulip Li-yao (May 11 2022 at 15:22):

Indeed there is no general way to run coqdoc on a package.

view this post on Zulip Brandon Moore (May 11 2022 at 16:01):

Too bad. At least coq_makefile has a target for it. Does dune? The closest I found was @doc but that only runs odoc and doesn't cover Coq files.

view this post on Zulip Ali Caglayan (May 11 2022 at 16:03):

Dune doesn't have a way to build doc with coqdoc (yet)

view this post on Zulip Ali Caglayan (May 11 2022 at 16:06):

We can however generate rules for coqdoc ourselves, and we will do this in the test-suite soon.

view this post on Zulip Ali Caglayan (May 11 2022 at 16:07):

It shouldn't be a huge leap to port that to dune.

view this post on Zulip Ali Caglayan (May 11 2022 at 16:08):

https://github.com/ocaml/dune/issues/3760

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 17:00):

That should be indeed very easy!

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 17:00):

I'll be happy to assist anyone interested in doing that

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 17:01):

First step is to write a rule .v -> .html this is trivial

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 17:01):

Second step is to take care of the deps

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 17:01):

likely a trivial step too, but you may need to add some flags to tell coqdoc where to find .glob files of other theories

view this post on Zulip Ali Caglayan (May 11 2022 at 17:13):

Don't you just pass the same flags as we do to coqc?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 18:22):

Ali Caglayan said:

Don't you just pass the same flags as we do to coqc?

we need to check as the logic in coqdoc is very different

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 18:22):

many flags are not accepted, so I'm unsure

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 18:22):

maybe instead of flags it expects a list of .glbo files?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 18:22):

composition / incremental build of docs is not easy actually, IIRC from odoc discussions

view this post on Zulip Ali Caglayan (May 11 2022 at 18:41):

coqdoc understands -Q and -R

view this post on Zulip Paolo Giarrusso (May 11 2022 at 19:46):

@Emilio Jesús Gallego Arias doc builds are AFAIK not incremental today, but they take negligible time compared to building vo files, so making the latter incremental is enough

view this post on Zulip Ali Caglayan (May 12 2022 at 08:39):

I've began an implementation, but it will not be incremental. coqdoc seems to do everything at once when called via coq_makefile, which gives it a separate html/ directory and creates a table of contents and index. I am trying to mimic the same in dune right now.

view this post on Zulip Ali Caglayan (May 12 2022 at 08:40):

With a few tweaks to coqdoc it could be possible to make an incremental build, but I am unsure how much desire there is for that.

view this post on Zulip Ali Caglayan (May 12 2022 at 08:40):

odoc support in dune is quite complicated, so it is not really worth sharing any work there.

view this post on Zulip Ali Caglayan (May 12 2022 at 08:41):

Another question is: What to do when there are multiple theory stanzas? At the moment coq_makefile shoves theories/ doc into html, but if there are multiple what then?

view this post on Zulip Ali Caglayan (May 12 2022 at 08:42):

There are various config options for coqdoc (html/latex, utf8 etc.) which we could add to the coq.theory stanza

view this post on Zulip Ali Caglayan (May 12 2022 at 08:43):

Here is the PR: https://github.com/ocaml/dune/pull/5695 currently ran into a dune issue which will need a separate fix first, so this is not the final form

view this post on Zulip Rudi Grinberg (May 19 2022 at 01:00):

For the issue of multiple theories, you probably want a directory target named theory.html or theory.latex


Last updated: Jan 29 2023 at 05:03 UTC