Skip to content

Commit e307464

Browse files
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 cbba1ca commit e307464

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

theories/dune

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
(include_subdirs qualified)
2+
3+
; We omit All.v as not to block on rocq-core build
24
(coq.theory
35
(name Stdlib)
4-
(package rocq-stdlib))
6+
(package rocq-stdlib)
7+
(modules :standard \ All))
58

69
(env
710
(dev
@@ -10,5 +13,5 @@
1013

1114
(rule
1215
(targets All.v)
13-
(deps All.sh (source_tree .))
16+
(deps (package rocq-core) All.sh (source_tree .))
1417
(action (with-stdout-to %{targets} (run env bash ./All.sh))))

0 commit comments

Comments
 (0)