54 lines
1.8 KiB
Diff
54 lines
1.8 KiB
Diff
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
|
|
|