Brandon Moore (May 11 2022 at 14:53): 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?
Li-yao (May 11 2022 at 15:22):Indeed there is no general way to run coqdoc on a package.
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.
Ali Caglayan (May 11 2022 at 16:03):Dune doesn't have a way to build doc with coqdoc (yet)
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.
Ali Caglayan (May 11 2022 at 16:07):It shouldn't be a huge leap to port that to dune.
Ali Caglayan (May 11 2022 at 16:08):https://github.com/ocaml/dune/issues/3760
Emilio Jesús Gallego Arias (May 11 2022 at 17:00):That should be indeed very easy!
Emilio Jesús Gallego Arias (May 11 2022 at 17:00):I'll be happy to assist anyone interested in doing that
Emilio Jesús Gallego Arias (May 11 2022 at 17:01):First step is to write a rule .v -> .html this is trivial
Emilio Jesús Gallego Arias (May 11 2022 at 17:01):Second step is to take care of the deps
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
Ali Caglayan (May 11 2022 at 17:13):Don't you just pass the same flags as we do to coqc?
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
Emilio Jesús Gallego Arias (May 11 2022 at 18:22):many flags are not accepted, so I'm unsure
Emilio Jesús Gallego Arias (May 11 2022 at 18:22):maybe instead of flags it expects a list of .glbo files?
Emilio Jesús Gallego Arias (May 11 2022 at 18:22):composition / incremental build of docs is not easy actually, IIRC from odoc discussions
Ali Caglayan (May 11 2022 at 18:41):coqdoc understands -Q and -R
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
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.
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.
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.
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?
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
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
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: Sep 23 2023 at 13:01 UTC