Merge PR coq#18287: [build] [opam] Pass -p correctly to `make dunestr…

…ap` so we don't rebuild things in coq-core Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <[email protected]>
eladrion · Nov 13, 2023 · b353daf · b353daf
2 parents a4d962e + 041633d
commit b353daf
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 19 deletions.
diff --git a/Makefile b/Makefile
@@ -118,10 +118,18 @@ help-install:
 	@echo " Note that building a package in release mode ignores other packages present in"
 	@echo " the worktree. See Dune documentation for more information."
 
+# We setup the root even in dev mode, to avoid some problems.  We used
+# this in the past to workaround a bug in opam, but the bug was that
+# we didn't pass `-p` to the dune build below.
+#
+# This would be fixed once dune can directly use `(include
+# theories_dune)` in our files.
+DUNESTRAPOPT=--root .
+
 # We regenerate always as to correctly track deps, can do better
 # We do a single call to dune as to avoid races and locking
 _build/default/theories_dune _build/default/ltac2_dune .dune-stamp: FORCE
-	dune build $(DUNEOPT) --root . theories_dune ltac2_dune
+	dune build $(DUNEOPT) $(DUNESTRAPOPT) theories_dune ltac2_dune
 	touch .dune-stamp
 
 theories/dune: .dune-stamp

diff --git a/coq-stdlib.opam b/coq-stdlib.opam
@@ -31,15 +31,8 @@ depopts: ["coq-native"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
-  # need to run configure as in coq-core, or else dunestrap will
-  # use the default rule in config
-  [ "./configure"
-    "-prefix" prefix
-    "-mandir" man
-    "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
-  ]
-  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]
+  # We tell dunestrap to use coq-config from coq-core
+  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"]
   [
     "dune"
     "build"

diff --git a/coq-stdlib.opam.template b/coq-stdlib.opam.template
@@ -1,14 +1,7 @@
 build: [
   ["dune" "subst"] {dev}
-  # need to run configure as in coq-core, or else dunestrap will
-  # use the default rule in config
-  [ "./configure"
-    "-prefix" prefix
-    "-mandir" man
-    "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
-  ]
-  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]
+  # We tell dunestrap to use coq-config from coq-core
+  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"]
   [
     "dune"
     "build"