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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
open Format
open Coqdep_lexer
open Coqdep_common
open Minisys
(** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
are now in [Coqdep_common]. The code that remains here concerns
the other options. Calling this complete coqdep with the [-boot]
option should be equivalent to calling [coqdep_boot].
As of today, this module depends on the following Coq modules:
- Envars
- CoqProject_file
All of it for `coqlib` handling. Ideally we would like to clean
coqlib handling up so this can be bootstrapped earlier.
*)
let option_sort = ref false
let warning_mult suf iter =
let tab = Hashtbl.create 151 in
let check f d =
begin try
let d' = Hashtbl.find tab f in
if (Filename.dirname (file_name f d))
<> (Filename.dirname (file_name f d')) then begin
coqdep_warning "the file %s is defined twice!" (f ^ suf)
end
with Not_found -> () end;
Hashtbl.add tab f d
in
iter check
let sort () =
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 coq_action lb with
| Require (from, sl) ->
List.iter
(fun s ->
match search_v_known ?from s with
| None -> ()
| Some f -> loop f)
sl
| _ -> ()
done
with Fin_fichier ->
close_in cin;
printf "%s%s " file !suffixe
end
in
List.iter (fun (name,_) -> loop name) !vAccu
let usage () =
eprintf " usage: coqdep [options] <filename>+\n";
eprintf " options:\n";
eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n";
eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
eprintf " -sort : output the given file name ordered by dependencies\n";
eprintf " -noglob | -no-glob : \n";
eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.";
eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n";
eprintf " -I dir : add (non recursively) dir to ocaml path\n";
eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *)
eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n";
eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n";
eprintf " -vos : also output dependencies about .vos files\n";
eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
eprintf " -coqlib dir : set the coq standard library directory\n";
eprintf " -suffix s : \n";
eprintf " -slash : deprecated, no effect\n";
eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
exit 1
let split_period = Str.split (Str.regexp (Str.quote "."))
let add_q_include path l = add_rec_dir_no_import add_known path (split_period l)
let add_r_include path l = add_rec_dir_import add_known path (split_period l)
let treat_coqproject f =
let open CoqProject_file in
let iter_sourced f = List.iter (fun {thing} -> f thing) in
let warning_fn x = coqdep_warning "%s" x in
let project = read_project_file ~warning_fn f in
iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes;
iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes;
iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes;
iter_sourced (fun f -> treat_file None f) (all_files project)
let rec parse = function
| "-c" :: ll -> option_c := true; parse ll
| "-boot" :: ll -> option_boot := true; parse ll
| "-sort" :: ll -> option_sort := true; parse ll
| "-vos" :: ll -> write_vos := true; parse ll
| ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
| "-f" :: f :: ll -> treat_coqproject f; parse ll
| "-I" :: r :: ll -> add_caml_dir r; parse ll
| "-I" :: [] -> usage ()
| "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll
| "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll
| "-R" :: ([] | [_]) -> usage ()
| "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll
| "-exclude-dir" :: [] -> usage ()
| "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll
| "-coqlib" :: [] -> usage ()
| "-suffix" :: s :: ll -> suffixe := s ; parse ll
| "-suffix" :: [] -> usage ()
| "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
| "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
| "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
| "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
| "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
| ("-h"|"--help"|"-help") :: _ -> usage ()
| f :: ll -> treat_file None f; parse ll
| [] -> ()
(* Exception to be raised by Envars *)
exception CoqlibError of string
let coqdep () =
if Array.length Sys.argv < 2 then usage ();
if not Coq_config.has_natdynlink then option_dynlink := No;
parse (List.tl (Array.to_list Sys.argv));
(* Add current dir with empty logical path if not set by options above. *)
(try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
with Not_found -> add_norec_dir_import add_known "." []);
(* NOTE: These directories are searched from last to first *)
if !option_boot then begin
add_rec_dir_import add_known "theories" ["Coq"];
add_rec_dir_import add_known "plugins" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
let user = "user-contrib" in
if Sys.file_exists user then begin
add_rec_dir_no_import add_known user [];
add_rec_dir_no_import (fun _ -> add_caml_known) user [];
end;
end else begin
(* option_boot is actually always false in this branch *)
Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
let user = coqlib//"user-contrib" in
if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
(Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x));
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu;
List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu;
warning_mult ".mli" iter_mli_known;
warning_mult ".ml" iter_ml_known;
if !option_sort then begin sort (); exit 0 end;
if !option_c then mL_dependencies ();
coq_dependencies ();
()
let _ =
try
coqdep ()
with CoqlibError msg ->
eprintf "*** Error: %s@\n%!" msg;
exit 1
|
