Merge PR #8443: [opam] [dune] Fix typo + set prefix for configure.

7 files changed, 24 insertions, 8 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 27d7fbf243..039c02c4b9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2018-09-20-V2"
+  CACHEKEY: "bionic_coq-V2018-09-21-V2"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/Makefile.dune b/Makefile.dune
index 81afa5bb91..cac1bdd6a1 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -7,6 +7,9 @@
 # DUNEOPT=--display=short
 
 BUILD_CONTEXT=_build/default
+COQ_CONFIGURE_PREFIX?=_build/install/default
+
+export COQ_CONFIGURE_PREFIX
 
 help:
 	@echo "Welcome to Coq's Dune-based build system. Targets are:"
diff --git a/config/dune b/config/dune
index 30faf1233e..cf2bc71363 100644
--- a/config/dune
+++ b/config/dune
@@ -9,5 +9,5 @@
 (rule
  (targets coq_config.ml)
  (mode fallback)
- (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run)
- (action (chdir %{project_root} (run %{ocaml} configure.ml -local -warn-error yes -native-compiler yes))))
+ (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -native-compiler no))))
diff --git a/configure.ml b/configure.ml
index 00ec559a1b..1c2edefc5c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1038,7 +1038,16 @@ let find_suffix prefix path = match prefix with
 let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) =
   let dir,suffix =
     if !prefs.local then (use_suffix coqtop locallayout,locallayout)
-    else match uservalue, !prefs.prefix with
+    else
+    let env_prefix =
+      match !prefs.prefix with
+      | None ->
+        begin
+          try Some (Sys.getenv "COQ_CONFIGURE_PREFIX")
+          with Not_found -> None
+        end
+      | p -> p
+    in match uservalue, env_prefix with
     | Some d, p -> d,find_suffix p d
     | _, Some p ->
       let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in
diff --git a/coq.opam b/coq.opam
index 7f577dd8be..cd89057598 100644
--- a/coq.opam
+++ b/coq.opam
@@ -15,8 +15,12 @@ depends: [
   "camlp5"
 ]
 
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+]
+
 build: [
   [ "dune" "build" "@vodeps" ]
   [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ]
-  [ "dune" "build" "-p" package "-j" jobs ]
+  [ "dune" "build" "-p" name "-j" jobs ]
 ]
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 9fad274bf4..d943795258 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-20-V2"
+# CACHEKEY: "bionic_coq-V2018-09-21-V2"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -34,7 +34,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \
     CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
diff --git a/ide/coqide.opam b/ide/coqide.opam
index 1b46efdee2..ba05b9edcf 100644
--- a/ide/coqide.opam
+++ b/ide/coqide.opam
@@ -16,4 +16,4 @@ depends: [
   "coq"
 ]
 
-build: [ [ "dune" "build" "-p" package "-j" jobs ] ]
+build: [ [ "dune" "build" "-p" name "-j" jobs ] ]