-
Notifications
You must be signed in to change notification settings - Fork 631
/
common.ml
372 lines (342 loc) · 13.5 KB
/
common.ml
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
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
(************************************************************************)
(* * 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 StrSet = Set.Make(String)
(** [basename_noext] removes both the directory part and the extension
(if necessary) of a filename *)
let basename_noext filename =
let fn = Filename.basename filename in
try Filename.chop_extension fn with Invalid_argument _ -> fn
(** Coq files specifies on the command line:
- first string is the full filename, with only its extension removed
- second string is the absolute version of the previous (via getcwd)
*)
let vAccu = ref ([] : (string * string) list)
let separator_hack = ref true
let filename_concat dir name =
if !separator_hack
then System.(dir // name)
else Filename.concat dir name
(* This is used to overcome makefile limitations w.r.t. filenames,
(bar/../foo is not the same than ./foo for make) but it is a crude
hack and we should remove it, and instead require users to follow
the same naming convention *)
let canonize f =
let f' = filename_concat (Loadpath.absolute_dir (Filename.dirname f)) (Filename.basename f) in
match List.filter (fun (_,full) -> f' = full) !vAccu with
| (f,_) :: _ -> f
| _ -> f
(** Queue operations *)
let addQueue q v = q := v :: !q
type what = Library | External
let str_of_what = function Library -> "library" | External -> "external file"
let warning_module_notfound =
let warn (what, from, f, s) =
let open Pp in
str "in file " ++ str f ++ str ", " ++
str (str_of_what what) ++ spc () ++ str (String.concat "." s) ++ str " is required" ++
pr_opt (fun pth -> str "from root " ++ str (String.concat "." pth)) from ++
str " and has not been found in the loadpath!"
in
CWarnings.create ~name:"module-not-found"
~category:CWarnings.CoreCategories.filesystem warn
let warning_declare =
let warn (f, s) =
let open Pp in
str "in file " ++ str f ++ str ", declared ML module " ++ str s ++
str " has not been found!"
in
CWarnings.create ~name:"declared-module-not-found"
~category:CWarnings.CoreCategories.filesystem warn
let warn_if_clash ?(what=Library) exact file dir f1 = let open Format in function
| f2::fl ->
let f =
match what with
| Library -> Filename.basename f1 ^ ".v"
| External -> Filename.basename f1 in
let what = str_of_what what in
let d1 = Filename.dirname f1 in
let d2 = Filename.dirname f2 in
let dl = List.rev_map Filename.dirname fl in
if exact then
begin
eprintf
"*** Warning: in file %s, \n required %s %s exactly matches several files in path\n (found %s in "
file what (String.concat "." dir) f;
List.iter (fun s -> eprintf "%s, " s) dl;
eprintf "%s and %s; used the latter).\n" d2 d1
end
else
begin
eprintf
"*** Warning: in file %s, \n required %s %s matches several files in path\n (found %s in "
file what (String.concat "." dir) f;
List.iter (fun s -> eprintf "%s, " s) dl;
eprintf "%s and %s; Require will fail).\n" d2 d1
end
| [] -> ()
let safe_assoc st ?(what=Library) from verbose file k =
let search =
match what with
| Library -> Loadpath.search_v_known st
| External -> Loadpath.search_other_known st in
match search ?from k with
| None -> None
| Some (Loadpath.ExactMatches (f :: l)) ->
if verbose then warn_if_clash ~what true file k f l; Some [f]
| Some (Loadpath.PartialMatchesInSameRoot (root, l)) ->
(match List.sort String.compare l with [] -> assert false | f :: l as all ->
(* If several files match, it will fail at Require;
To be "fair", in coqdep, we add dependencies on all matching files *)
if verbose then warn_if_clash ~what false file k f l; Some all)
| Some (Loadpath.ExactMatches []) -> assert false
let file_name s = function
| None -> s
| Some d -> filename_concat d s
module VData = struct
type t = string list option * string list
let compare = compare
end
module VCache = Set.Make(VData)
(** To avoid reading .v files several times for computing dependencies,
once for .vo, once for .vio, and once for .vos extensions, the
following code performs a single pass and produces a structured
list of dependencies, separating dependencies on compiled Coq files
(those loaded by [Require]) from other dependencies, e.g. dependencies
on ".v" files (for [Load]) or ".cmx", ".cmo", etc... (for [Declare]). *)
let legacy_mapping = Core_plugins_findlib_compat.legacy_to_findlib
let meta_files = ref []
(* Transform "Declare ML %DECL" to a pair of (meta, cmxs). Something
very similar is in ML top *)
let declare_ml_to_file file decl =
let decl = String.split_on_char ':' decl in
let decl = List.map (String.split_on_char '.') decl in
let meta_files = !meta_files in
match decl with
| [[x]] when List.mem_assoc x legacy_mapping ->
None, x (* This case only exists for 3rd party packages, should remove in 8.17 *)
| [[x]] ->
Error.findlib_name file x
| [[legacy]; package :: plugin_name] ->
None, legacy
| [package :: plugin_name] ->
let meta, cmxs = Fl.findlib_resolve ~meta_files ~file ~package ~plugin_name in
Some meta, cmxs
| plist ->
CErrors.user_err
Pp.(str "Failed to resolve plugin " ++
pr_sequence (pr_sequence str) plist)
let rec find_dependencies st basename =
let verbose = true in (* for past/future use? *)
try
(* Visited marks *)
let visited_ml = ref StrSet.empty in
let visited_v = ref VCache.empty in
let should_visit_v_and_mark from str =
if not (VCache.mem (from, str) !visited_v) then begin
visited_v := VCache.add (from, str) !visited_v;
true
end else false
in
(* Output: dependencies found *)
let dependencies = ref [] in
let add_dep dep = dependencies := dep :: !dependencies in
let add_dep_other s = add_dep (Dep_info.Dep.Other s) in
(* Reading file contents *)
let f = basename ^ ".v" in
let chan = open_in f in
let buf = Lexing.from_channel chan in
let open Lexer in
try
while true do
let tok = coq_action buf in
match tok with
| Require (from, strl) ->
let decl str =
if should_visit_v_and_mark from str then begin
match safe_assoc st from verbose f str with
| Some files ->
List.iter (fun file_str ->
let file_str = canonize file_str in
add_dep (Dep_info.Dep.Require file_str)) files
| None ->
if verbose && not (Loadpath.is_in_coqlib st ?from str) then
warning_module_notfound (Library, from, f, str)
end
in
List.iter decl strl
| Declare sl ->
let sl = List.map (declare_ml_to_file f) sl in
let declare suff dir s =
let base = file_name s dir in
add_dep (Dep_info.Dep.Ml (base,suff))
in
let decl (meta_file,str) =
Option.iter add_dep_other meta_file;
let s = basename_noext str in
if not (StrSet.mem s !visited_ml) then begin
visited_ml := StrSet.add s !visited_ml;
let pick_mldir mldir =
match meta_file with
| None -> mldir
| Some _ -> Some(Filename.dirname str)
in
match Loadpath.search_mllib_known st s with
| Some mldir -> declare ".cma" (pick_mldir mldir) s
| None ->
match Loadpath.search_mlpack_known st s with
| Some mldir -> declare ".cmo" (pick_mldir mldir) s
| None -> warning_declare (f,str)
end
in
List.iter decl sl
| Load file ->
let canon =
match file with
| Logical str ->
if should_visit_v_and_mark None [str] then safe_assoc st None verbose f [str]
else None
| Physical str ->
if String.equal (Filename.basename str) str then
if should_visit_v_and_mark None [str] then safe_assoc st None verbose f [str]
else None
else
Some [canonize str]
in
(match canon with
| None -> ()
| Some l ->
let decl canon =
add_dep_other (Format.sprintf "%s.v" canon);
let deps = find_dependencies st canon in
List.iter add_dep deps
in
List.iter decl l)
| External(from,str) ->
begin match safe_assoc st ~what:External (Some from) verbose f [str] with
| Some (file :: _) -> add_dep (Dep_info.Dep.Other (canonize file))
| Some [] -> assert false
| None -> warning_module_notfound (External, Some from, f, [str])
end
done;
List.rev !dependencies
with
| Fin_fichier ->
close_in chan;
List.rev !dependencies
| Syntax_error (i,j) ->
close_in chan;
Error.cannot_parse f (i,j)
with Sys_error msg -> Error.cannot_open (basename ^ ".v") msg
module State = struct
type t = Loadpath.State.t
let loadpath x = x
end
let compute_deps st =
let mk_dep (name, _orig_path) = Dep_info.make ~name ~deps:(find_dependencies st name) in
!vAccu |> List.rev |> List.map mk_dep
let rec treat_file old_dirname old_name =
let name = Filename.basename old_name
and new_dirname = Filename.dirname old_name in
let dirname =
match (old_dirname,new_dirname) with
| (d, ".") -> d
(* EGJA: We should disable this buggy normalization stuff for
"./foo -> foo" but it breaks dune coq.theory! *)
| (None,d) -> Some d
| (Some d1,d2) -> Some (filename_concat d1 d2)
in
let complete_name = file_name name dirname in
let stat_res =
try Unix.stat complete_name
with Unix.Unix_error(error, _, _) ->
Error.cannot_open complete_name (Unix.error_message error)
in
match stat_res.Unix.st_kind with
| Unix.S_DIR ->
(if name.[0] <> '.' then
let newdirname =
match dirname with
| None -> name
| Some d -> filename_concat d name
in
Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
| Unix.S_REG ->
(match Loadpath.get_extension name [".v"] with
| base,".v" ->
let name = file_name base dirname in
let absname = Loadpath.absolute_file_name ~filename_concat base dirname in
addQueue vAccu (name, absname)
| _ -> ())
| _ -> ()
let treat_file_command_line old_name =
treat_file None old_name
let treat_file_coq_project where old_name =
treat_file None old_name
(* "[sort]" outputs `.v` files required by others *)
let sort st =
let seen = Hashtbl.create 97 in
let rec loop file =
let file = canonize file in
if not (Hashtbl.mem seen file) then begin
Hashtbl.add seen file ();
let cin = open_in (file ^ ".v") in
let lb = Lexing.from_channel cin in
try
while true do
match Lexer.coq_action lb with
| Lexer.Require (from, sl) ->
List.iter
(fun s ->
match safe_assoc st from false file s with
| None -> ()
| Some l -> List.iter loop l)
sl
| _ -> ()
done
with Lexer.Fin_fichier ->
close_in cin;
Format.printf "%s.v " file
end
in
List.iter (fun (name, _) -> loop name) !vAccu
let warn_project_file =
let category = CWarnings.CoreCategories.filesystem in
CWarnings.create ~name:"project-file" ~category Pp.str
let treat_coqproject st f =
let open CoqProject_file in
let iter_sourced f = List.iter (fun {thing} -> f thing) in
let project =
try read_project_file ~warning_fn:warn_project_file f
with
| Parsing_error msg -> Error.cannot_parse_project_file f msg
| UnableToOpenProjectFile msg -> Error.cannot_open_project_file msg
in
iter_sourced (fun { path } -> Loadpath.add_caml_dir st path) project.ml_includes;
iter_sourced (fun ({ path }, l) -> Loadpath.add_q_include st path l) project.q_includes;
iter_sourced (fun ({ path }, l) -> Loadpath.add_r_include st path l) project.r_includes;
iter_sourced (fun f' -> treat_file_coq_project f f') (all_files project)
let add_include st (rc, r, ln) =
if rc then
Loadpath.add_r_include st r ln
else
Loadpath.add_q_include st r ln
let init ~make_separator_hack args =
separator_hack := make_separator_hack;
vAccu := [];
if not Coq_config.has_natdynlink then Makefile.set_dyndep "no";
let st = Loadpath.State.make ~boot:args.Args.boot in
Makefile.set_write_vos args.Args.vos;
Makefile.set_noglob args.Args.noglob;
Option.iter (treat_coqproject st) args.Args.coqproject;
List.iter (Loadpath.add_caml_dir st) args.Args.ml_path;
List.iter (add_include st) args.Args.vo_path;
Makefile.set_dyndep args.Args.dyndep;
meta_files := args.Args.meta_files;
st