Skip to content

Commit

Permalink
[build] Set dune root explicitly / use --release
Browse files Browse the repository at this point in the history
This should fix coq#14915 , the problem arises with layouts of the form:

```
foo/dune-project
foo/_opam/bar/dune-project
```

so when inside `foo/_opam/bar`, dune will switch to `foo` as the
project root, for example for `dune build` or `dune exec` , however,
as `_opam` is an ignored dir by default in the `foo` context, the
command will fail.

So indeed, it turns out `--profile release` is not enough, but
`--release` must be used when configured for install.

Thanks a lot to Kate for the help!
  • Loading branch information
ejgallego committed Sep 22, 2021
1 parent cb113c3 commit 4d966c4
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion Makefile.common
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ DOCGRAM_SOURCE_FILES=$(shell find $(addprefix $(COQ_SRC_DIR)/, doc/tools/docgram
# Override for developer build [to get warn-as-error for example]
_DDISPLAY?=quiet
_DPROFILE?=$(CONFIGURE_DPROFILE)
_DOPT:=--display $(_DDISPLAY) --profile=$(_DPROFILE)
_DOPT:=--display=$(_DDISPLAY) $(_DPROFILE)
_DBUILD:=$(FLOCK) .dune.lock dune build $(_DOPT)

# We rerun dune when any of the source files have changed
Expand Down
2 changes: 1 addition & 1 deletion configure
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ then
exit 1
fi

dune exec -- $configure "$@"
dune exec --root . -- $configure "$@"
4 changes: 2 additions & 2 deletions tools/configure/cmdArgs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -71,15 +71,15 @@ let default = {
if os_type_win32 || os_type_cygwin then NativeNo else NativeOndemand;
coqwebsite = "http://coq.inria.fr/";
warn_error = false;
dune_profile = "release";
dune_profile = "--release";
install_enabled = true;
}

let devel state = { state with
bin_annot = true;
annot = true;
warn_error = true;
dune_profile = "dev";
dune_profile = "--profile=dev";
interactive = true;
prefix = Some (Filename.concat (Sys.getcwd ()) "_build_vo/default");
install_enabled = false;
Expand Down

0 comments on commit 4d966c4

Please sign in to comment.