[dune] [configure] Allow to set prefix using environment variable.

This is a hack to enable correct OPAM building, the medium-term plan
is to avoid having to set a prefix at configure time but instead using
a set of rules to locate the Coq library.

We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2

6 files changed, 22 insertions, 6 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 e04982650f..2d303b9846 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 2ac98d8946..cd89057598 100644
--- a/coq.opam
+++ b/coq.opam
@@ -15,6 +15,10 @@ depends: [
   "camlp5"
 ]
 
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+]
+
 build: [
   [ "dune" "build" "@vodeps" ]
   [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ]
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.