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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
type t =
{ coqlib : string
; vo_load_path : Loadpath.vo_path list
; ml_include_path : string list
; require_libs :
(string * string option * Vernacexpr.export_with_cats option) list
; indices_matter : bool
; impredicative_set : bool
; kind : string
; debug : bool
}
let default ~implicit ~coqlib ~kind ~debug =
let mk_path prefix = coqlib ^ "/" ^ prefix in
let mk_lp ~ml ~root ~dir ~implicit =
{ Loadpath.unix_path = mk_path dir
; coq_path = root
; has_ml = ml
; implicit
; recursive = true
}
in
let coq_root = Names.DirPath.make [ Libnames.coq_root ] in
let default_root = Libnames.default_root_prefix in
let require_libs = [ ("Coq.Init.Prelude", None, Some (Lib.Import, None)) ] in
{ coqlib
; vo_load_path =
[ mk_lp ~ml:false ~root:coq_root ~implicit ~dir:"theories"
; mk_lp ~ml:true ~root:default_root ~implicit:false ~dir:"user-contrib"
]
; ml_include_path =
(let unix_path = Filename.concat coqlib "../coq-core/plugins" in
System.all_subdirs ~unix_path |> List.map fst)
; require_libs
; indices_matter = false
; impredicative_set = false
; kind
; debug
}
let add_loadpaths base ~vo_load_path ~ml_include_path =
{ base with
vo_load_path = base.vo_load_path @ vo_load_path
; ml_include_path = base.ml_include_path @ ml_include_path
}
let pp_load_path fmt
{ Loadpath.unix_path; coq_path; implicit = _; has_ml = _; recursive = _ } =
Format.fprintf fmt "Path %s ---> %s"
(Names.DirPath.to_string coq_path)
unix_path
let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } =
let require_msg =
String.concat " " (List.map (fun (s, _, _) -> s) require_libs)
in
let n_vo = List.length vo_load_path in
let n_ml = List.length ml_include_path in
let =
Format.asprintf "@[vo_paths:@\n @[<v>%a@]@\nml_paths:@\n @[<v>%a@]@]"
(Format.pp_print_list pp_load_path)
vo_load_path
Format.(pp_print_list pp_print_string)
ml_include_path
in
( Format.asprintf
"@[Configuration loaded from %s@\n\
\ - coqlib is at: %s@\n\
\ - Modules [%s] will be loaded by default@\n\
\ - %d Coq path directory bindings in scope; %d Coq plugin directory \
bindings in scope@]"
kind coqlib require_msg n_vo n_ml
, extra )
let rec parse_args args init w =
match args with
| [] -> (init, w)
| "-indices-matter" :: rest ->
parse_args rest init { w with indices_matter = true }
| "-impredicative-set" :: rest ->
parse_args rest init { w with impredicative_set = true }
| "-noinit" :: rest -> parse_args rest false w
| _ :: rest ->
parse_args rest init w
let load_objs libs =
let rq_file (dir, from, exp) =
let mp = Libnames.qualid_of_string dir in
let mfrom = Option.map Libnames.qualid_of_string from in
Flags.silently
(Vernacentries.vernac_require mfrom exp)
[ (mp, Vernacexpr.ImportAll) ]
in
List.(iter rq_file (rev libs))
let dirpath_of_file f =
let ldir0 =
try
let lp = Loadpath.find_load_path (Filename.dirname f) in
Loadpath.logical lp
with Not_found -> Libnames.default_root_prefix
in
let f =
try Filename.chop_extension (Filename.basename f)
with Invalid_argument _ -> f
in
let id = Names.Id.of_string f in
let ldir = Libnames.add_dirpath_suffix ldir0 id in
ldir
let dirpath_of_uri ~uri =
let file =
if String.length uri > 8 then
let l = String.length uri - 7 in
String.(sub uri 7 l)
else uri
in
dirpath_of_file file
let apply ~uri
{ coqlib = _
; vo_load_path
; ml_include_path
; require_libs
; indices_matter
; impredicative_set
; kind = _
; debug
} =
if debug then CDebug.set_flags "backtrace";
Global.set_indices_matter indices_matter;
Global.set_impredicative_set impredicative_set;
List.iter Mltop.add_ml_dir ml_include_path;
List.iter Loadpath.add_vo_path vo_load_path;
Declaremods.start_library (dirpath_of_uri ~uri);
load_objs require_libs
let workspace_from_coqproject ~coqlib ~debug cp_file : t =
let open CoqProject_file in
let to_vo_loadpath f implicit =
let open Loadpath in
let unix_path, coq_path = f in
{ implicit
; recursive = true
; has_ml = false
; unix_path = unix_path.path
; coq_path = Libnames.dirpath_of_string coq_path
}
in
let { r_includes; q_includes; ml_includes; ; _ } =
read_project_file ~warning_fn:(fun _ -> ()) cp_file
in
let ml_include_path = List.map (fun f -> f.thing.path) ml_includes in
let vo_path = List.map (fun f -> to_vo_loadpath f.thing false) q_includes in
let vo_load_path =
List.append vo_path
(List.map (fun f -> to_vo_loadpath f.thing true) r_includes)
in
let args = List.map (fun f -> f.thing) extra_args in
let implicit = true in
let kind = Filename.concat (Sys.getcwd ()) "_CoqProject" in
let workspace = default ~coqlib ~implicit ~kind ~debug in
let init, workspace = parse_args args true workspace in
let workspace =
if not init then { workspace with require_libs = [] } else workspace
in
add_loadpaths workspace ~vo_load_path ~ml_include_path
module CmdLine = struct
type t =
{ coqlib : string
; vo_load_path : Loadpath.vo_path list
; ml_include_path : string list
}
end
let workspace_from_cmdline ~debug
{ CmdLine.coqlib; vo_load_path; ml_include_path } =
let kind = "Command-line arguments" in
let implicit = true in
let w = default ~implicit ~coqlib ~kind ~debug in
add_loadpaths w ~vo_load_path ~ml_include_path
let guess ~debug ~cmdline ~dir =
let cp_file = Filename.concat dir "_CoqProject" in
if Sys.file_exists cp_file then
workspace_from_coqproject ~coqlib:cmdline.CmdLine.coqlib ~debug cp_file
else workspace_from_cmdline ~debug cmdline