[coqdep] Remove dumpgraph and broken options

We remove the `dumpgraph` option which was causing quite a bit of
duplication, we also clean up options marked as broken `-w/-D`

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