diff --git a/Makefile b/Makefile index 0c5fa14f7c1f..9b0e42ca1048 100644 --- 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 index 3cb83999c000..ca56a8bb4876 100644 --- 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 index 352d17b3038e..e554bec966c4 100644 --- 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"