From f720f0dddaf28505fde192e5912ffa63817d3122 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Dec 2020 11:26:43 +0100 Subject: [coq_makefile] honor environment for OCAMLFIND --- lib/envars.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/envars.ml b/lib/envars.ml index 585d5185b4..0455e8305b 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -145,7 +145,7 @@ let coqpath = (** {2 Caml paths} *) -let ocamlfind () = Coq_config.ocamlfind +let ocamlfind () = getenv_else "OCAMLFIND" (fun () -> Coq_config.ocamlfind) (** {1 XDG utilities} *) -- cgit v1.2.3 From 4c4715bf3224f6750e8d63005ff0c554015db45e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Dec 2020 11:27:15 +0100 Subject: [coq_makefile] use Envars for COQMF_WINDRIVE --- tools/coq_makefile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3 From 1b39124d33f609740bb601ee5468f39470ba540b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Dec 2020 10:10:14 +0100 Subject: [doc] coq_environment.txt --- INSTALL.md | 10 ++++++++++ 1 file changed, 10 insertions(+) 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. -- cgit v1.2.3 From 823a5a0ca12e574fa4d9851f76b28d0a78baa118 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Nov 2020 15:06:21 +0100 Subject: [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. --- lib/envars.ml | 32 +++++++++++++++++++++++- test-suite/misc/coq_environment.sh | 51 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 82 insertions(+), 1 deletion(-) create mode 100755 test-suite/misc/coq_environment.sh 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 < /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 -- cgit v1.2.3 From 957fba5a176f74b397a3adf7c008e63145617b66 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Dec 2020 15:05:22 +0100 Subject: [test-suite] improve ocaml_pwd --- test-suite/ocaml_pwd.ml | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) 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 -- cgit v1.2.3 From 9fb840fa5f33f593bc204765a13c027155559c2e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Dec 2020 15:05:40 +0100 Subject: [dune] [test-suite] pass BIN= as the regular makefile does --- test-suite/dune | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/test-suite/dune b/test-suite/dune index 6ab2988331..1864153021 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -8,6 +8,10 @@ (targets libpath.inc) (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 @@ -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}")))) -- cgit v1.2.3