blob: 6c48224c6458c26f29aab1e242cecaa79be084ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
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
|
