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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
module Path = struct
type t = string
let relative = Filename.concat
let to_string x = x
let exists x = Sys.file_exists x
end
(* For now just a pointer to coq/lib (for .vo) and coq-core/lib (for plugins) *)
type t =
{ core: Path.t
; lib : Path.t
}
(* fatal error *)
let fail_msg =
"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 fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1
(* This code needs to be refactored, for now it is just what used to be in envvars *)
let theories_dir = "theories"
let plugins_dir = "plugins"
let prelude = Filename.concat theories_dir "Init/Prelude.vo"
let guess_coqlib () =
Util.getenv_else "COQLIB" (fun () ->
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 ()))
(* Build layout uses coqlib = coqcorelib *)
let guess_coqcorelib lib =
if Sys.file_exists (Path.relative lib plugins_dir)
then lib
else Path.relative lib "../coq-core"
let fail_lib lib =
let open Printf in
eprintf "File not found: %s\n" lib;
eprintf "The path for Coq libraries is wrong.\n";
eprintf "Coq libraries are shipped in the coq-stdlib package.\n";
eprintf "Please check the COQLIB env variable or the -coqlib option.\n";
exit 1
let fail_core plugin =
let open Printf in
eprintf "File not found: %s\n" plugin;
eprintf "The path for Coq plugins is wrong.\n";
eprintf "Coq plugins are shipped in the coq-core package.\n";
eprintf "Please check the COQCORELIB env variable.\n";
exit 1
let validate_env ({ core; lib } as env) =
let lib = Filename.concat lib prelude in
if not (Sys.file_exists lib) then fail_lib lib;
let plugin = Filename.concat core plugins_dir in
if not (Sys.file_exists plugin) then fail_core plugin;
env
(* Should we fail on double initialization? That seems a way to avoid
mis-use for example when we pass command line arguments *)
let init () =
let lib = guess_coqlib () in
let core = Util.getenv_else "COQCORELIB"
(fun () -> guess_coqcorelib lib) in
validate_env { core ; lib }
let env_ref = ref None
let init () =
match !env_ref with
| None ->
let env = init () in
env_ref := Some env; env
| Some env -> env
let set_coqlib lib =
let env = validate_env { lib; core = guess_coqcorelib lib } in
env_ref := Some env
let coqlib { lib; _ } = lib
let corelib { core; _ } = core
let plugins { core; _ } = Path.relative core plugins_dir
let stdlib { lib; _ } = Path.relative lib theories_dir
let user_contrib { lib; _ } = Path.relative lib "user-contrib"
let tool { core; _ } tool = Path.(relative (relative core "tools") tool)
let revision { core; _ } = Path.relative core "revision"
let native_cmi { core; _ } lib =
let install_path = Path.relative core lib in
if Sys.file_exists install_path then
install_path
else
(* Dune build layout, we need to improve this *)
let obj_dir = Format.asprintf ".%s.objs" lib in
Filename.(concat (concat (concat core lib) obj_dir) "byte")
|
