7 files changed, 136 insertions, 20 deletions
diff --git a/INSTALL.md b/INSTALL.md
index f672bb45d3..74f4091134 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -99,3 +99,13 @@ dependencies...) as Coq.  Distribution of pre-compiled plugins and
 Coq version compiled with the same OCaml toolchain.  An OCaml setup
 mismatch is the most probable cause for an `Error while loading ...:
 implementation mismatch on ...`.
+
+coq_environment.txt
+-------------------
+Coq binaries which honor environment variables, such as `COQLIB`, can
+be seeded values for these variables by placing a text file named
+`coq_environment.txt` next to them. The file can contain assignments
+like `COQLIB="some path"`, that is a variable name followed by `=` and
+a string that follows OCaml's escaping conventions. This feature can be
+used by installers of binary package to make Coq aware of its installation
+path.
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 14ee5e4199..cf1d71c1cd 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -5,27 +5,29 @@ have prepared a branch with the fix, you can add an "overlay" to your pull
 request to test it with the adapted version of the external project.
 
 An overlay is a file which defines where to look for the patched
-version so that testing is possible. This is done by calling the
-`overlay` command for each project with the project name (as used in
-the variables in [`ci-basic-overlay.sh`](../ci-basic-overlay.sh)), the
-location of your fork and the branch containing the patch on your
-fork.
-
-Moreover, the file contains very simple logic to test the pull request number
-or branch name and apply it only in this case.
-
+version so that testing is possible.
 The name of your overlay file should start with a five-digit pull request
 number, followed by a dash, anything (for instance your GitHub nickname
 and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 
-Example: `13128-SkySkimmer-noinstance.sh` containing
+This file must contain one or more invocation of the `overlay` function:
+```
+overlay <project> <giturl> <ref> <prnumber> [<prbranch>]
+```
+Each call creates an overlay for `project` using a given `giturl` and
+`ref` which is active for `prnumber` or `prbranch` (`prbranch` defaults
+to `ref`).
 
+Example of an overlay for the project `elpi` that uses the branch `noinstance`
+from the fork of `SkySkimmer` and is active for pull request `13128`
 ```
 overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128
 ```
 
-See [`ci-common.sh`](../ci-common.sh) for the detailed documentation of
-the `overlay` function.
+Such a file can be created automatically using the scripts
+[`create_overlays.sh`](../../dev/tools/create_overlays.sh).
+See also the list of projects for which one can write an overlay in
+the file [`ci-basic-overlay.sh`](../ci-basic-overlay.sh).
 
 ### Branching conventions
 
diff --git a/lib/envars.ml b/lib/envars.ml
index 585d5185b4..1702b5d7a2 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -12,7 +12,37 @@ open Util
 
 (** {1 Helper functions} *)
 
-let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
+let parse_env_line l =
+  try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
+  with _ -> None
+
+let with_ic file f =
+  let ic = open_in file in
+  try
+    let rc = f ic in
+    close_in ic;
+    rc
+  with e -> close_in ic; raise e
+
+let getenv_from_file name =
+  let base = Filename.dirname Sys.executable_name in
+  try
+    with_ic (base ^ "/coq_environment.txt") (fun ic ->
+      let rec find () =
+        let l = input_line ic in
+        match parse_env_line l with
+        | Some(n,v) when n = name -> v
+        | _ -> find ()
+      in
+        find ())
+  with
+  | Sys_error s -> raise Not_found
+  | End_of_file -> raise Not_found
+
+let system_getenv name =
+  try Sys.getenv name with Not_found -> getenv_from_file name
+
+let getenv_else s dft = try system_getenv s with Not_found -> dft ()
 
 let safe_getenv warning n =
   getenv_else n (fun () ->
@@ -145,7 +175,7 @@ let coqpath =
 
 (** {2 Caml paths} *)
 
-let ocamlfind () = Coq_config.ocamlfind
+let ocamlfind () = getenv_else "OCAMLFIND" (fun () -> Coq_config.ocamlfind)
 
 (** {1 XDG utilities} *)
 
diff --git a/test-suite/dune b/test-suite/dune
index 6ab2988331..1864153021 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -9,6 +9,10 @@
  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
 
 (rule
+ (targets bin.inc)
+ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
+
+(rule
  (targets summary.log)
  (deps
    ; File that should be promoted.
@@ -44,4 +48,4 @@
    ; %{bin:fake_ide}
  (action
   (progn
-   (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
+   (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
new file mode 100755
index 0000000000..667d11f89e
--- /dev/null
+++ b/test-suite/misc/coq_environment.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+TMP=`mktemp -d`
+cd $TMP
+
+cat > coq_environment.txt <<EOT
+# we override COQLIB because we can
+COQLIB="$TMP/overridden" # bla bla
+OCAMLFIND="$TMP/overridden"
+FOOBAR="one more"
+EOT
+
+cp $BIN/coqc .
+cp $BIN/coq_makefile .
+mkdir -p overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+
+unset COQLIB
+N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo OCAMLFIND not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+./coq_makefile -o CoqMakefile -R . foo > /dev/null
+N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQMF_OCAMLFIND not overridden by coq_environment
+  cat CoqMakefile.conf
+  exit 1
+fi
+
+export COQLIB="/overridden2"
+N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by COQLIB when coq_environment present
+  coqc -config
+  exit 1
+fi
+
+rm -rf $TMP
+exit 0
diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml
index afa3deea3a..054a921b93 100644
--- a/test-suite/ocaml_pwd.ml
+++ b/test-suite/ocaml_pwd.ml
@@ -1,7 +1,26 @@
+open Arg
+
+let quoted = ref false
+let trailing_slash = ref false
+
+let arguments = [
+  "-quoted",Set quoted, "Quote path";
+  "-trailing-slash",Set trailing_slash, "End the path with a /";
+]
+let subject = ref None
+let set_subject x =
+  if !subject <> None then
+    failwith "only one path";
+  subject := Some x
+
 let _ =
-  let quoted = Sys.argv.(1) = "-quoted" in
-  let ch_dir = Sys.argv.(if quoted then 2 else 1) in
-  Sys.chdir ch_dir;
+  Arg.parse arguments set_subject "Usage:";
+  let subject =
+    match !subject with
+    | None -> failwith "no path given";
+    | Some x -> x in
+  Sys.chdir subject;
   let dir = Sys.getcwd () in
-  let dir = if quoted then Filename.quote dir else dir in
+  let dir = if !trailing_slash then dir ^ "/" else dir in
+  let dir = if !quoted then Filename.quote dir else dir in
   Format.printf "%s%!" dir
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0cbfd46e80..07550b67e3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -216,7 +216,7 @@ let generate_conf_coq_config oc =
   section oc "Coq configuration.";
   let src_dirs = Coq_config.all_src_dirs in
   Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
-  fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
+  fprintf oc "COQMF_WINDRIVE=%s\n" (windrive (Envars.coqlib()))
 ;;
 
 let generate_conf_files oc