Fixed #4407.

Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.

4 files changed, 74 insertions, 31 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 110d306022..e0e017e88a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -426,8 +426,9 @@ let coq_dependencies_dump chan dumpboxes =
 end
 
 let usage () =
-  eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n";
+  eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-Q dir coqdir] [-R dir coqdir] <filename>+\n";
   eprintf " extra options:\n";
+  eprintf "  -sort : output the file names ordered by dependencies\n";
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -exclude-dir f : skip subdirectories named 'f' during -R search\n";
   eprintf "  -dumpgraph f : print a dot dependency graph in file 'f'\n";
@@ -442,16 +443,17 @@ let rec parse = function
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
-  | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [];
-    add_dir add_known r (split_period ln);
-    parse ll
+  | "-I" :: r :: "-as" :: ln :: ll ->
+     add_rec_dir_no_import add_known r [];
+     add_rec_dir_no_import add_known r (split_period ln);
+     parse ll
   | "-I" :: r :: "-as" :: [] -> usage ()
   | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
-  | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
+  | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
   | "-R" :: r :: "-as" :: [] -> usage ()
-  | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
-  | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll
+  | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
+  | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period 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
@@ -471,23 +473,26 @@ let rec parse = function
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   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 "." []);
   if not Coq_config.has_natdynlink then option_natdynlk := false;
   (* NOTE: These directories are searched from last to first *)
   if !option_boot then begin
-    add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"];
-    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
+    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"];
   end else begin
     Envars.set_coqlib ~fail:Errors.error;
     let coqlib = Envars.coqlib () in
-    add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
-    add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
+    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_dir add_coqlib_known user [];
-    List.iter (fun s -> add_dir add_coqlib_known s [])
+    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 (fun x -> Pp.msg_warning (Pp.str x)));
-    List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath;
+    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;
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 64ce66d2d1..088ea6bfcf 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -35,15 +35,15 @@ let _ =
   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 add_known "." [];
-    add_rec_dir (fun _ -> add_caml_known) "." ["Coq"];
+    add_rec_dir_import add_known "." [];
+    add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"];
   end
   else begin
-    add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"];
+    add_rec_dir_import add_known "theories" ["Coq"];
+    add_rec_dir_import add_known "plugins" ["Coq"];
     add_caml_dir "tactics";
-    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
+    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 ca42c99470..02fd19a1e2 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -220,6 +220,18 @@ let absolute_file_name basename odir =
   let dir = match odir with Some dir -> dir | None -> "." in
   absolute_dir dir // basename
 
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+    if it has been given one. Raise [Not_found] otherwise. In
+    particular we can check if "." has been attributed a logical path
+    after processing all options and silently give the default one if
+    it hasn't. We may also use this to warn if ap hysical path is met
+    twice.*)
+let register_dir_logpath,find_dir_logpath =
+  let tbl: (string, string list) Hashtbl.t = Hashtbl.create 19 in
+  let reg physdir logpath = Hashtbl.add tbl (absolute_dir physdir) logpath in
+  let fnd physdir = Hashtbl.find tbl (absolute_dir physdir) in
+  reg,fnd
+
 let file_name s = function
   | None     -> s
   | Some "." -> s
@@ -339,7 +351,8 @@ let escape =
     Buffer.contents s'
 
 let compare_file f1 f2 =
-  absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2)
+  absolute_file_name (Filename.basename f1) (Some (Filename.dirname f1))
+  = absolute_file_name (Filename.basename f2) (Some (Filename.dirname f2))
 
 let canonize f =
   let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
@@ -514,11 +527,13 @@ let add_known recur phys_dir log_dir f =
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
-(* Visits all the directories under [dir], including [dir],
-   or just [dir] if [recur=false] *)
-
+(** Visit directory [phys_dir] (recursively unless [recur=false]) and
+    apply function add_file to each regular file encountered.
+    [log_dir] is the logical name of the [phys_dir].
+    [add_file] takes both directory names and the file. *)
 let rec add_directory recur add_file phys_dir log_dir =
   let dirh = opendir phys_dir in
+  register_dir_logpath phys_dir log_dir;
   try
     while true do
       let f = readdir dirh in
@@ -531,19 +546,24 @@ let rec add_directory recur add_file phys_dir log_dir =
               if StrSet.mem f !norec_dirnames then ()
               else
 	        if StrSet.mem phys_f !norec_dirs then ()
-	        else
+	        else (* TODO: warn if already seen this physycal dir? *)
 		  add_directory recur add_file phys_f (log_dir@[f])
 	  | S_REG -> add_file phys_dir log_dir f
 	  | _ -> ()
     done
   with End_of_file -> closedir dirh
 
+(** Simply add this directory and imports it, no subdirs. This is used
+    by the implicit adding of the current path (which is not recursive). *)
+let add_norec_dir_import add_file phys_dir log_dir =
+  try add_directory false (add_file true) phys_dir log_dir with Unix_error _ -> ()
+
 (** -Q semantic: go in subdirs but only full logical paths are known. *)
-let add_dir add_file phys_dir log_dir =
+let add_rec_dir_no_import add_file phys_dir log_dir =
   try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
 
 (** -R semantic: go in subdirs and suffixes of logical paths are known. *)
-let add_rec_dir add_file phys_dir log_dir =
+let add_rec_dir_import add_file phys_dir log_dir =
   handle_unix_error (add_directory true (add_file true) phys_dir) log_dir
 
 (** -I semantic: do not go in subdirs. *)
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index d610a0558d..50cae40d9a 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -8,6 +8,14 @@
 
 module StrSet : Set.S with type elt = string
 
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+    if it has been given one. Raise [Not_found] otherwise. In
+    particular we can check if "." has been attributed a logical path
+    after processing all options and silently give the default one if
+    it hasn't. We may also use this to warn if ap hysical path is met
+    twice.*)
+val find_dir_logpath: string -> string list
+
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
@@ -47,9 +55,19 @@ val add_directory :
   bool ->
   (string -> string list -> string -> unit) -> string -> string list -> unit
 val add_caml_dir : string -> unit
-val add_dir :
+
+(** Simply add this directory and imports it, no subdirs. This is used
+    by the implicit adding of the current path. *)
+val add_norec_dir_import :
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
+(** -Q semantic: go in subdirs but only full logical paths are known. *)
+val add_rec_dir_no_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-val add_rec_dir :
+
+(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
+val add_rec_dir_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
 val treat_file : dir -> string -> unit
 val error_cannot_parse : string -> int * int -> 'a