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
)
Not at the moment, it could be added however.
Please create a ticket in the dune repo.
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.
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.
@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.
@Rodolphe Lepigre note that --trace-file can provide similar info than your time script
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
.
That's probably something that is of general interest in Dune for other things so I wil make sure to mention it
https://github.com/ocaml/dune/issues/7595
Please add any more usecases if you have some in mind
@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 .
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.
btw dune 3.8 has coqdoc_flags as a field to the coq stanza.
the default value :standard is --toc
you should be able to put your own flags in there now
@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.
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.
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: Oct 13 2024 at 01:02 UTC