Merge PR #11523: [coqdep] Several refactoring and consolidations

Reviewed-by: SkySkimmer
Ack-by: gares

4 files changed, 9 insertions, 448 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2140014c58..745cf950b5 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -20,7 +20,6 @@ open Minisys
 
     As of today, this module depends on the following Coq modules:
 
-    - Flags
     - Envars
     - CoqProject_file
 
@@ -28,10 +27,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 +70,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 +84,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";
@@ -468,7 +94,6 @@ let usage () =
 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 =
@@ -482,9 +107,8 @@ let treat_coqproject f =
   iter_sourced (fun f -> treat_file None f) (all_files project)
 
 let rec parse = function
+  (* TODO, deprecate option -c *)
   | "-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,17 +119,12 @@ 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
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
-  | "-slash" :: ll ->
-    coqdep_warning "warning: option -slash has no effect and is deprecated.";
-    parse ll
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
   | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
@@ -525,19 +144,8 @@ let coqdep () =
   (* 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 *)
+  (* We don't setup any loadpath if the -boot is passed *)
+  if not !option_boot then begin
     Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
     let coqlib = Envars.coqlib () in
     add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
@@ -554,17 +162,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
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 1730dd3d68..1cebb3638e 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -19,6 +19,7 @@ open Coqdep_common
 
 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 rec parse = function
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
@@ -26,16 +27,14 @@ let rec parse = function
   | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
   | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
   | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
-  | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
-  | "-mldep" :: ocamldep :: ll ->
-      option_mldep := Some ocamldep; option_c := true; parse ll
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
        add_caml_dir r;
        norec_dirs := StrSet.add r !norec_dirs;
        parse ll
+  | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll
   | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
@@ -44,16 +43,4 @@ let _ =
   let () = option_boot := true in
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
-  if !option_c then begin
-    add_rec_dir_import add_known "." [];
-    add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"];
-  end
-  else begin
-    add_rec_dir_import add_known "theories" ["Coq"];
-    add_rec_dir_import add_known "plugins" ["Coq"];
-    add_caml_dir "tactics";
-    add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
-  end;
-  if !option_c then mL_dependencies ();
   coq_dependencies ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 775c528176..bd72a52adf 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -35,7 +35,6 @@ let option_c = ref false
 let option_noglob = ref false
 let option_dynlink = ref Both
 let option_boot = ref false
-let option_mldep = ref None
 
 let norec_dirs = ref StrSet.empty
 
@@ -246,26 +245,7 @@ let depend_ML str =
         (" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
-let soustraite_fichier_ML dep md ext =
-  try
-    let chan = open_process_in (dep^" -modules "^md^ext) in
-    let list = ocamldep_parse (Lexing.from_channel chan) in
-    let a_faire = ref "" in
-    let a_faire_opt = ref "" in
-    List.iter
-      (fun str ->
-         let byte,opt = depend_ML str in
-         a_faire := !a_faire ^ byte;
-         a_faire_opt := !a_faire_opt ^ opt)
-      (List.rev list);
-    (!a_faire, !a_faire_opt)
-  with
-    | Sys_error _ -> ("","")
-    | _ ->
-       Printf.eprintf "Coqdep: subprocess %s failed on file %s%s\n" dep md ext;
-       exit 1
-
-let autotraite_fichier_ML md ext =
+let traite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
@@ -290,11 +270,6 @@ let autotraite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
-let traite_fichier_ML md ext =
-  match !option_mldep with
-    | Some dep -> soustraite_fichier_ML dep md ext
-    | None -> autotraite_fichier_ML md ext
-
 let traite_fichier_modules md ext =
   try
     let chan = open_in (md ^ ext) in
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 6d49f7e06c..96266b8e36 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -30,7 +30,6 @@ val write_vos : bool ref
 type dynlink = Opt | Byte | Both | No | Variable
 
 val option_dynlink : dynlink ref
-val option_mldep : string option ref
 val norec_dirs : StrSet.t ref
 val suffixe : string ref
 type dir = string option