From 8f23d8d339403006d6464510c7d2cd285cf38b0a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Sep 2018 10:46:09 +0200
Subject: [opam] Fix typo in build variable.

Fixes #8431
---
 coq.opam        | 2 +-
 ide/coqide.opam | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq.opam b/coq.opam
index 7f577dd8be..2ac98d8946 100644
--- a/coq.opam
+++ b/coq.opam
@@ -18,5 +18,5 @@ depends: [
 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/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 ] ]
-- 
cgit v1.2.3


From 81e4c7152da598c1750e7881b197a6fcf54e818d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Sep 2018 11:37:09 +0200
Subject: [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
---
 .gitlab-ci.yml                      |  2 +-
 Makefile.dune                       |  3 +++
 config/dune                         |  4 ++--
 configure.ml                        | 11 ++++++++++-
 coq.opam                            |  4 ++++
 dev/ci/docker/bionic_coq/Dockerfile |  4 ++--
 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.
-- 
cgit v1.2.3