[win] [envars] honor file "coq_environment.txt"

On windows we provide a way to set environment variables
local to a coq installation by providing a file
named "coq_environment.txt" containing KEY="value" pairs.

No space between KEY and = is allowed, values are in
quotes according to OCaml's escaping conventions.
The file is line-directed, illformed lines are skipped.

2 files changed, 82 insertions, 1 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 0455e8305b..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 () ->
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