From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001 From: Julien Lepiller <julien@lepiller.eu> Date: Thu, 10 Feb 2022 16:44:10 +0100 Subject: [PATCH] Fix environment variable usage. --- boot/env.ml | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/boot/env.ml b/boot/env.ml index e8521e7..d834a3a 100644 --- a/boot/env.ml +++ b/boot/env.ml @@ -32,17 +32,29 @@ let fail_msg = let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1 +let path_to_list p = + let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in + String.split_on_char sep p + (* This code needs to be refactored, for now it is just what used to be in envvars *) let guess_coqlib () = Util.getenv_else "COQLIB" (fun () -> let prelude = "theories/Init/Prelude.vo" in - Util.check_file_else - ~dir:Coq_config.coqlibsuffix - ~file:prelude - (fun () -> - if Sys.file_exists (Filename.concat Coq_config.coqlib prelude) - then Coq_config.coqlib - else fail ())) + let coqlibpath = Util.getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in + let paths = path_to_list coqlibpath in + let valid_paths = + List.filter + (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "") + paths in + match valid_paths with + | [] -> + if Sys.file_exists (Filename.concat Coq_config.coqlib prelude) + then Coq_config.coqlib + else + fail "cannot guess a path for Coq libraries; please use -coqlib option \ + or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \ + If you intend to use Coq without a standard library, the -boot -noinit options must be used." + | p::_ -> p) (* Build layout uses coqlib = coqcorelib *) let guess_coqcorelib lib = -- 2.34.0