Stream: Dune devs & users

Topic: Passing flags to coqdoc


view this post on Zulip Armaël Guéneau (Apr 14 2023 at 22:41):

Is there a way to pass coqdoc flags when using dune? (I'm currently building the docs for a coq.theory by doing dune build @doc)

view this post on Zulip Ali Caglayan (Apr 17 2023 at 09:07):

Not at the moment, it could be added however.

view this post on Zulip Ali Caglayan (Apr 17 2023 at 09:07):

Please create a ticket in the dune repo.

view this post on Zulip Ali Caglayan (Apr 17 2023 at 09:08):

I know some people have ways of passing flags by making a wrapper script. Perhaps @Paolo Giarrusso or @Rodolphe Lepigre can say more how this can work.

view this post on Zulip Rodolphe Lepigre (Apr 17 2023 at 09:11):

Yeah, that's a trick I came up with while working on RefinedC: https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tools/coqc_timing.sh.
Note that in the script you need to use opam exec -- coqc or something similar, to not just get a fork-bomb.

view this post on Zulip Ali Caglayan (Apr 17 2023 at 09:17):

@Armaël Guéneau btw which flags are you trying to pass to coqdoc? One of the reasons I didn't just add a (coqdoc_flags) field yet is because behind the scenes Dune is passing things like --latex separetely since you have the @doc and @doc-latex aliases. If I allow users to pass whatever flags, I need to make sure that things are not broken.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 20 2023 at 16:42):

@Rodolphe Lepigre note that --trace-file can provide similar info than your time script

view this post on Zulip Rodolphe Lepigre (Apr 20 2023 at 18:18):

Cool, I had no idea this existed! However, that would not do for us since (I think) it only reports timing information, which is unreliable for performance measurements. We really want instruction counts, and the wrapper script can do that when combined with Linux perf.

view this post on Zulip Ali Caglayan (Apr 20 2023 at 18:25):

That's probably something that is of general interest in Dune for other things so I wil make sure to mention it

view this post on Zulip Ali Caglayan (Apr 20 2023 at 18:27):

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

view this post on Zulip Ali Caglayan (Apr 20 2023 at 18:27):

Please add any more usecases if you have some in mind

view this post on Zulip Armaël Guéneau (Jun 07 2023 at 07:26):

@Ali Caglayan sorry to be coming back late to this. The flags I was trying to pass to coqdoc were similar to what is done here: https://github.com/logsem/cerise/blob/main/Makefile#L2 .

view this post on Zulip Rodolphe Lepigre (Jun 07 2023 at 08:11):

It'd be cool if the --external bits could be done automatically for you, based on some documentation URL in the opam file of the packages you depend on, or additional meta-data of some kind that dune could generate in the opam files it controls.

view this post on Zulip Ali Caglayan (Jun 07 2023 at 12:00):

btw dune 3.8 has coqdoc_flags as a field to the coq stanza.

view this post on Zulip Ali Caglayan (Jun 07 2023 at 12:00):

the default value :standard is --toc

view this post on Zulip Ali Caglayan (Jun 07 2023 at 12:00):

you should be able to put your own flags in there now

view this post on Zulip Ali Caglayan (Jun 07 2023 at 12:01):

@Rodolphe Lepigre having external flags configurable in the stanza seems like a sensible option. Could you detail it in an issue and I'll see about implementing it.

view this post on Zulip Rodolphe Lepigre (Jun 07 2023 at 12:08):

See https://github.com/ocaml/dune/issues/7912. That is what I had in mind, but something simpler could also be good to start with.

view this post on Zulip Ali Caglayan (Jun 07 2023 at 12:22):

Interesting proposal, I'll have to think about it more in depth. There are similar happenings for odoc at the moment, so I want to see how they handle things.


Last updated: May 25 2024 at 19:02 UTC