diff options
| -rw-r--r-- | man/coqdep.1 | 31 | ||||
| -rw-r--r-- | tools/coqdep.ml | 391 |
2 files changed, 4 insertions, 418 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1 index 02c9d4390c..4223482c99 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -6,9 +6,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .SH SYNOPSIS .B coqdep [ -.BI \-w -] -[ .BI \-I \ directory ] [ @@ -21,9 +18,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .BI \-i ] [ -.BI \-D -] -[ .BI \-slash ] .I filename ... @@ -61,25 +55,6 @@ directives and the dot notation .BI \-c Prints the dependencies of Caml modules. (On Caml modules, the behaviour is exactly the same as ocamldep). -\" THESE OPTIONS ARE BROKEN CURRENTLY -\" .TP -\" .BI \-w -\" Prints a warning if a Coq command -\" .IR Declare \& -\" .IR ML \& -\" .IR Module \& -\" is incorrect. (For instance, you wrote `Declare ML Module "A".', -\" but the module A contains #open "B"). The correct command is printed -\" (see option \-D). The warning is printed on standard error. -\" .TP -\" .BI \-D -\" This commands looks for every command -\" .IR Declare \& -\" .IR ML \& -\" .IR Module \& -\" of each Coq file given as argument and complete (if needed) -\" the list of Caml modules. The new command is printed on -\" the standard output. No dependency is computed with this option. .TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. @@ -93,10 +68,6 @@ Indicates where is the Coq library. The default value has been determined at installation time, and therefore this option should not be used under normal circumstances. .TP -.BI \-dumpgraph[box] \ file -Dumps a dot dependency graph in file -.IR file \&. -.TP .BI \-exclude-dir \ dir Skips subdirectory .IR dir \ during @@ -169,7 +140,7 @@ example% coqdep \-I . *.v With a warning: .IP .B -example% coqdep \-w \-I . *.v +example% coqdep \-I . *.v .RS .sp .5 .nf diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2140014c58..fcafd826f0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -28,10 +28,7 @@ open Minisys coqlib handling up so this can be bootstrapped earlier. *) -let option_D = ref false -let option_w = ref false let option_sort = ref false -let option_dump = ref None let warning_mult suf iter = let tab = Hashtbl.create 151 in @@ -74,378 +71,10 @@ let sort () = in List.iter (fun (name,_) -> loop name) !vAccu -let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151 - -let mL_dep_list b f = - try - Hashtbl.find dep_tab f - with Not_found -> - let deja_vu = ref ([] : string list) in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - try - while true do - let (Use_module str) = caml_action buf in - if str = b then begin - coqdep_warning "in file %s the notation %s. is useless !\n" f b - end else - if not (List.mem str !deja_vu) then addQueue deja_vu str - done; [] - with Fin_fichier -> begin - close_in chan; - let rl = List.rev !deja_vu in - Hashtbl.add dep_tab f rl; - rl - end - with Sys_error _ -> [] - -let affiche_Declare f dcl = - printf "\n*** In file %s: \n" f; - printf "Declare ML Module"; - List.iter (fun str -> printf " \"%s\"" str) dcl; - printf ".\n%!" - -let warning_Declare f dcl = - eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f; - eprintf "*** Declare ML Module"; - List.iter (fun str -> eprintf " \"%s\"" str) dcl; - eprintf ".\n%!" - -let traite_Declare f = - let decl_list = ref ([] : string list) in - let rec treat = function - | s :: ll -> - let s' = basename_noext s in - (match search_ml_known s with - | Some mldir when not (List.mem s' !decl_list) -> - let fullname = file_name s' mldir in - let depl = mL_dep_list s (fullname ^ ".ml") in - treat depl; - decl_list := s :: !decl_list - | _ -> ()); - treat ll - | [] -> () - in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - begin try - while true do - let tok = coq_action buf in - (match tok with - | Declare sl -> - decl_list := []; - treat sl; - decl_list := List.rev !decl_list; - if !option_D then - affiche_Declare f !decl_list - else if !decl_list <> sl then - warning_Declare f !decl_list - | _ -> ()) - done - with Fin_fichier -> () end; - close_in chan - with Sys_error _ -> () - -let declare_dependencies () = - List.iter - (fun (name,_) -> - traite_Declare (name^".v"); - pp_print_flush std_formatter ()) - (List.rev !vAccu) - -(** DAGs guaranteed to be transitive reductions *) -module DAG (Node : Set.OrderedType) : -sig - type node = Node.t - type t - val empty : t - val add_transitive_edge : node -> node -> t -> t - val iter : (node -> node -> unit) -> t -> unit -end = -struct - type node = Node.t - module NSet = Set.Make(Node) - module NMap = Map.Make(Node) - - (** Associate to a node the set of its neighbours *) - type _t = NSet.t NMap.t - - (** Optimisation: construct the reverse graph at the same time *) - type t = { dir : _t; rev : _t; } - - - let node_equal x y = Node.compare x y = 0 - - let add_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - NMap.add x (NSet.add y set) graph - - let remove_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - let set = NSet.remove y set in - if NSet.is_empty set then NMap.remove x graph - else NMap.add x set graph - - let has_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - NSet.mem y set - - let connected x y graph = - let rec aux rem seen = - if NSet.is_empty rem then false - else - let x = NSet.choose rem in - if node_equal x y then true - else - let rem = NSet.remove x rem in - if NSet.mem x seen then - aux rem seen - else - let seen = NSet.add x seen in - let next = try NMap.find x graph with Not_found -> NSet.empty in - let rem = NSet.union next rem in - aux rem seen - in - aux (NSet.singleton x) NSet.empty - - (** Check whether there is a path from a to b going through the edge - x -> y. *) - let connected_through a b x y graph = - let rec aux rem seen = - if NMap.is_empty rem then false - else - let (n, through) = NMap.choose rem in - if node_equal n b && through then true - else - let rem = NMap.remove n rem in - let is_seen = try Some (NMap.find n seen) with Not_found -> None in - match is_seen with - | None -> - let seen = NMap.add n through seen in - let next = try NMap.find n graph with Not_found -> NSet.empty in - let is_x = node_equal n x in - let push m accu = - let through = through || (is_x && node_equal m y) in - NMap.add m through accu - in - let rem = NSet.fold push next rem in - aux rem seen - | Some false -> - (* The path we took encountered x -> y but not the one in seen *) - if through then aux (NMap.add n true rem) (NMap.add n true seen) - else aux rem seen - | Some true -> aux rem seen - in - aux (NMap.singleton a false) NMap.empty - - let closure x graph = - let rec aux rem seen = - if NSet.is_empty rem then seen - else - let x = NSet.choose rem in - let rem = NSet.remove x rem in - if NSet.mem x seen then - aux rem seen - else - let seen = NSet.add x seen in - let next = try NMap.find x graph with Not_found -> NSet.empty in - let rem = NSet.union next rem in - aux rem seen - in - aux (NSet.singleton x) NSet.empty - - let empty = { dir = NMap.empty; rev = NMap.empty; } - - (** Online transitive reduction algorithm *) - let add_transitive_edge x y graph = - if connected x y graph.dir then graph - else - let dir = add_edge x y graph.dir in - let rev = add_edge y x graph.rev in - let graph = { dir; rev; } in - let ancestors = closure x rev in - let descendents = closure y dir in - let fold_ancestor a graph = - let fold_descendent b graph = - let to_remove = has_edge a b graph.dir in - let to_remove = to_remove && not (node_equal x a && node_equal y b) in - let to_remove = to_remove && connected_through a b x y graph.dir in - if to_remove then - let dir = remove_edge a b graph.dir in - let rev = remove_edge b a graph.rev in - { dir; rev; } - else graph - in - NSet.fold fold_descendent descendents graph - in - NSet.fold fold_ancestor ancestors graph - - let iter f graph = - let iter x set = NSet.iter (fun y -> f x y) set in - NMap.iter iter graph.dir - -end - -module Graph = -struct -(** Dumping a dependency graph **) - -module DAG = DAG(struct type t = string let compare = compare end) - -(** TODO: we should share this code with Coqdep_common *) -module VData = struct - type t = string list option * string list - let compare = Util.pervasives_compare -end - -module VCache = Set.Make(VData) - -let treat_coq_file chan = - let buf = Lexing.from_channel chan in - let deja_vu_v = ref VCache.empty in - let deja_vu_ml = ref StrSet.empty in - let mark_v_done from acc str = - let seen = VCache.mem (from, str) !deja_vu_v in - if not seen then - let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in - match search_v_known ?from str with - | None -> acc - | Some file_str -> (canonize file_str, !suffixe) :: acc - else acc - in - let rec loop acc = - let token = try Some (coq_action buf) with Fin_fichier -> None in - match token with - | None -> acc - | Some action -> - let acc = match action with - | Require (from, strl) -> - List.fold_left (fun accu v -> mark_v_done from accu v) acc strl - | Declare sl -> - let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> [] - | Byte -> [base,suff] - | Opt -> [base,".cmxs"] - | Both -> [base,suff; base,".cmxs"] - | Variable -> - if suff=".cmo" then [base,"$(DYNOBJ)"] - else [base,"$(DYNLIB)"] - in - let decl acc str = - let s = basename_noext str in - if not (StrSet.mem s !deja_vu_ml) then - let () = deja_vu_ml := StrSet.add s !deja_vu_ml in - match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) @ acc - | None -> - match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) @ acc - | None -> acc - else acc - in - List.fold_left decl acc sl - | Load str -> - let str = Filename.basename str in - let seen = VCache.mem (None, [str]) !deja_vu_v in - if not seen then - let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in - match search_v_known [str] with - | None -> acc - | Some file_str -> (canonize file_str, ".v") :: acc - else acc - | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *) - in - loop acc - in - loop [] - -let treat_coq_file f = - let chan = try Some (open_in f) with Sys_error _ -> None in - match chan with - | None -> [] - | Some chan -> - try - let ans = treat_coq_file chan in - let () = close_in chan in - ans - with Syntax_error (i, j) -> close_in chan; error_cannot_parse f (i, j) - -type graph = - | Element of string - | Subgraph of string * graph list - -let rec insert_graph name path graphs = match path, graphs with - | [] , graphs -> (Element name) :: graphs - | (box :: boxes), (Subgraph (hd, names)) :: tl when hd = box -> - Subgraph (hd, insert_graph name boxes names) :: tl - | _, hd :: tl -> hd :: (insert_graph name path tl) - | (box :: boxes), [] -> [ Subgraph (box, insert_graph name boxes []) ] - -let print_graphs chan graph = - let rec print_aux name = function - | [] -> name - | (Element str) :: tl -> fprintf chan "\"%s\";\n" str; print_aux name tl - | Subgraph (box, names) :: tl -> - fprintf chan "subgraph cluster%n {\nlabel=\"%s\";\n" name box; - let name = print_aux (name + 1) names in - fprintf chan "}\n"; print_aux name tl - in - ignore (print_aux 0 graph) - -let rec pop_common_prefix = function - | [Subgraph (_, graphs)] -> pop_common_prefix graphs - | graphs -> graphs - -let split_path = Str.split (Str.regexp "/") - -let rec pop_last = function - | [] -> [] - | [ x ] -> [] - | x :: xs -> x :: pop_last xs - -let get_boxes path = pop_last (split_path path) - -let insert_raw_graph file = - insert_graph file (get_boxes file) - -let rec get_dependencies name args = - let vdep = treat_coq_file (name ^ ".v") in - let fold (deps, graphs, alseen) (dep, _) = - let dag = DAG.add_transitive_edge name dep deps in - if not (List.mem dep alseen) then - get_dependencies dep (dag, insert_raw_graph dep graphs, dep :: alseen) - else - (dag, graphs, alseen) - in - List.fold_left fold args vdep - -let coq_dependencies_dump chan dumpboxes = - let (deps, graphs, _) = - List.fold_left (fun ih (name, _) -> get_dependencies name ih) - (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu, - List.map fst !vAccu) !vAccu - in - fprintf chan "digraph dependencies {\n"; - if dumpboxes then print_graphs chan (pop_common_prefix graphs) - else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu; - DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps; - fprintf chan "}\n%!" - -end - let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; - (* Does not work anymore *) - (* eprintf " -w : Print informations on missing or wrong \"Declare - ML Module\" commands in coq files.\n"; *) - (* Does not work anymore: *) - (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\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"; @@ -456,8 +85,6 @@ let usage () = 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 " -dumpgraph f : print a dot dependency graph in file 'f'\n"; - eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\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"; @@ -483,8 +110,6 @@ let treat_coqproject f = let rec parse = function | "-c" :: ll -> option_c := true; parse ll - | "-D" :: ll -> option_D := true; parse ll - | "-w" :: ll -> option_w := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll @@ -495,8 +120,6 @@ let rec parse = function | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | "-R" :: ([] | [_]) -> usage () - | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll - | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll @@ -554,17 +177,9 @@ let coqdep () = warning_mult ".mli" iter_mli_known; warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; - if !option_c && not !option_D then mL_dependencies (); - if not !option_D then coq_dependencies (); - if !option_w || !option_D then declare_dependencies (); - begin match !option_dump with - | None -> () - | Some (box, file) -> - let chan = open_out file in - let chan_fmt = formatter_of_out_channel chan in - try Graph.coq_dependencies_dump chan_fmt box; close_out chan - with e -> close_out chan; raise e - end + if !option_c then mL_dependencies (); + coq_dependencies (); + () let _ = try |