Commit 2447669
committed
[build] Fix missing deps in dune rule for All.v file
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.1 parent 418d350 commit 2447669
1 file changed
+5
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
| 2 | + | |
| 3 | + | |
2 | 4 | | |
3 | 5 | | |
4 | | - | |
| 6 | + | |
| 7 | + | |
5 | 8 | | |
6 | 9 | | |
7 | 10 | | |
| |||
10 | 13 | | |
11 | 14 | | |
12 | 15 | | |
13 | | - | |
| 16 | + | |
14 | 17 | | |
0 commit comments