[build] Fix missing deps in dune rule for All.v file

[ejgallego]

This fixes a bug for composed builds introduced in #167.

Re-submission of #188, which was merged and reverted.

As the rule stands, dune will try to generate the All.v file before both rocq and Corelib.Init.Prelude.vo have been built, which are both needed for the script.

Unfortunately, given the way rocq and prelude work, we need to depend on the full rocq-core package, so things are in the expected places before the generation of All.v.

This would linearize the stdlib build: we cannot run coqdep now for the Stdlib until the whole rocq-core package is built.

We could mitigate this by excluding All.v from the list of modules in the Stdlib coq.theory file (done in the patch), however, this won't install / build All.vo, so we should decide what the desired tradeoff is here.

[proux01]

IIUC, this means default dune build will skip All.v? I don't have any strong opinion against that but other may have one (Cc @andres-erbsen for instance)
If we do this, the CI script in Rocq repo should probably be updated to keep compiling (and testing) All.v in some way or another.

Disclaimer: I still don't really understand the issue here and the interaction with rocq-core (for me Stdlib obviously depends on rocq-core and I fail to see how this can be an issue) so maybe you shouldn't listen too much to me.

[SkySkimmer]

Could we avoid needing Prelude.vo when running the script? It doesn't seem like a fundamental need.

[andres-erbsen]

I also don't understand the details here. I do see value in having a fine-grained parallel build, but I am not sure it's worth excluding All.v to achieve that. Based on my current understanding, I can imagine only merging (deps (package rocq-core) All.sh (source_tree .)) but not the other changes.

Unfortunately, given the way rocq and prelude work, we need to depend on the full rocq-core package, so things are in the expected places before the generation of All.v.

My reading: due to current technical limitations (of dune? of coq-core dune rules?) we cannot have All.v depend on coqdep without depending on the entire package. Why is that, and is there an issue for it?

This would linearize the stdlib build

I am not sure what you mean - could files in stdlib still build in parallel?

we cannot run coqdep now for the Stdlib until the whole rocq-core package is built.

this might just be fine? what is the difference in critical-path build time?

Thank you for looking after our build,
Andres

[andres-erbsen]

Per #106 (comment), an alternatice solution might be to

• generated unsorted All.v without depending on coqdep
• in test suite, generate sorted All.v with correct dependencies

Or alternatively, only have the unsorted one.

• @proux01 why is it important to have that file topologically sorted? I have been thinking that it is to correctly attribute notation conflicts.
• @ejgallego which of these solutions would work for you?