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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Sun, 21 Nov 2021 00:38:03 +0100
Subject: [PATCH] Fix environment variable usage.
---
checker/checker.ml | 2 ++
lib/envars.ml | 26 ++++++++++++++++----------
sysinit/coqargs.ml | 3 ++-
sysinit/coqloadpath.ml | 3 ++-
sysinit/coqloadpath.mli | 2 +-
tools/coqdep.ml | 2 +-
6 files changed, 24 insertions(+), 14 deletions(-)
diff --git a/checker/checker.ml b/checker/checker.ml
index f55ed9e8d6..3b797729ed 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -104,6 +104,7 @@ let set_include d p =
(* Initializes the LoadPath *)
let init_load_path () =
let coqlib = Envars.coqlib () in
+ let coqcorelib = Envars.coqcorelib () in
let user_contrib = coqlib/"user-contrib" in
let xdg_dirs = Envars.xdg_dirs in
let coqpath = Envars.coqpath in
@@ -111,6 +112,7 @@ let init_load_path () =
CPath.choose_existing
[ CPath.make [ coqlib ; "plugins" ]
; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ]
+ ; CPath.make [ coqcorelib ; "plugins" ]
] |> function
| None ->
CErrors.user_err (Pp.str "Cannot find plugins directory")
diff --git a/lib/envars.ml b/lib/envars.ml
index 750bd60e71..c7affbd437 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -127,15 +127,21 @@ let check_file_else ~dir ~file oth =
let guess_coqlib fail =
getenv_else "COQLIB" (fun () ->
let prelude = "theories/Init/Prelude.vo" in
- check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
- (fun () ->
- if Sys.file_exists (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.")
- )
+ let coqlibpath = getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in
+ let paths = path_to_list coqlibpath in
+ let valid_paths =
+ List.filter
+ (fun dir -> (check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "")
+ paths in
+ match valid_paths with
+ | [] ->
+ if Sys.file_exists (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)
let coqlib_ref : string option ref = ref None
let set_user_coqlib path = coqlib_ref := Some path
@@ -208,7 +214,7 @@ let xdg_dirs ~warn =
let print_config ?(prefix_var_name="") f coq_src_subdirs =
let open Printf in
fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
- fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqlib () / "../coq-core/");
+ fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqcorelib ());
fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 00f70a5fea..8325623a63 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -453,7 +453,8 @@ let build_load_path opts =
if opts.pre.boot then [],[]
else
let coqlib = Envars.coqlib () in
- Coqloadpath.init_load_path ~coqlib in
+ let coqcorelib = Envars.coqcorelib () in
+ Coqloadpath.init_load_path ~coqlib ~coqcorelib in
ml_path @ opts.pre.ml_includes ,
vo_path @ opts.pre.vo_includes
diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml
index 95ae5da3de..a58cfe6928 100644
--- a/sysinit/coqloadpath.ml
+++ b/sysinit/coqloadpath.ml
@@ -35,7 +35,7 @@ let build_userlib_path ~unix_path =
else [], []
(* LoadPath for Coq user libraries *)
-let init_load_path ~coqlib =
+let init_load_path ~coqlib ~coqcorelib =
let open Loadpath in
let user_contrib = coqlib/"user-contrib" in
@@ -50,6 +50,7 @@ let init_load_path ~coqlib =
CPath.choose_existing
[ CPath.make [ coqlib ; "plugins" ]
; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ]
+ ; CPath.make [ coqcorelib ; "plugins" ]
] |> function
| None ->
CErrors.user_err (Pp.str "Cannot find plugins directory")
diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli
index d853e9ea54..43c6dfa134 100644
--- a/sysinit/coqloadpath.mli
+++ b/sysinit/coqloadpath.mli
@@ -12,5 +12,5 @@
includes (in-order) Coq's standard library, Coq's [user-contrib]
folder, and directories specified in [COQPATH] and [XDG_DIRS] *)
val init_load_path
- : coqlib:CUnix.physical_path
+ : coqlib:CUnix.physical_path -> coqcorelib:CUnix.physical_path
-> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index c1c87993e1..6c78e10866 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -33,7 +33,7 @@ let coqdep () =
let coqlib = Envars.coqlib () in
let coq_plugins_dir = Filename.concat (Envars.coqcorelib ()) "plugins" in
if not (Sys.file_exists coq_plugins_dir) then
- CErrors.user_err Pp.(str "coqdep: cannot find plugins directory for coqlib: " ++ str coqlib ++ fnl ());
+ CErrors.user_err Pp.(str "coqdep: cannot find plugins directory " ++ str coq_plugins_dir ++ str " for coqlib: " ++ str coqlib ++ fnl ());
CD.add_rec_dir_import CD.add_coqlib_known (coqlib//"theories") ["Coq"];
CD.add_rec_dir_import CD.add_coqlib_known (coq_plugins_dir) ["Coq"];
let user = coqlib//"user-contrib" in
--
2.33.1
|
