From 1546532d1a3e1c8bcccdbe08f5bff37e0cfd0c5c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 9 Jul 2025 17:11:00 +0200 Subject: [PATCH 1/2] [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. --- theories/dune | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/theories/dune b/theories/dune index 2f10c05ab0..8cf8b0c161 100644 --- a/theories/dune +++ b/theories/dune @@ -1,7 +1,10 @@ (include_subdirs qualified) + +; We omit All.v as not to block on rocq-core build (coq.theory (name Stdlib) - (package rocq-stdlib)) + (package rocq-stdlib) + (modules :standard \ All)) (env (dev @@ -11,5 +14,5 @@ (rule (targets All.v) - (deps All.sh (source_tree .)) + (deps (package rocq-core) All.sh (source_tree .)) (action (with-stdout-to %{targets} (run env bash ./All.sh)))) From a8c913b782e2e714d1490458ea9aedffb66e831d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 8 Sep 2025 17:31:33 +0200 Subject: [PATCH 2/2] [stdlib] Restore warning-free build. --- theories/dune | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/dune b/theories/dune index 8cf8b0c161..eadfb0093e 100644 --- a/theories/dune +++ b/theories/dune @@ -4,6 +4,14 @@ (coq.theory (name Stdlib) (package rocq-stdlib) + (flags + :standard + -w -deprecated-exact-proof + -w -deprecated-end-tac + -w -implicit-create-hint-db + -w -closed-notation-not-level-0 + -w -notation-for-abbreviation + -w -postfix-notation-not-level-1) (modules :standard \ All)) (env