Merge branch 'v8.5' into trunk

5 files changed, 74 insertions, 46 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f1a3131dd8..397ccd8a25 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -56,11 +56,12 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require sl ->
+	    | Require (from, sl) ->
 		List.iter
 		  (fun s ->
-		    try loop (Hashtbl.find vKnown s)
-		    with Not_found -> ())
+                    match search_v_known ?from s with
+                    | None -> ()
+                    | Some f -> loop f)
 		sl
 	    | _ -> ()
 	done
@@ -299,16 +300,15 @@ module DAG = DAG(struct type t = string let compare = compare end)
 (** TODO: we should share this code with Coqdep_common *)
 let treat_coq_file chan =
   let buf = Lexing.from_channel chan in
-  let deja_vu_v = ref ([]: string list list)
+  let deja_vu_v = ref ([]: (string list option * string list) list)
   and deja_vu_ml = ref ([] : string list) in
-  let mark_v_done acc str =
-    let seen = List.mem str !deja_vu_v in
+  let mark_v_done from acc str =
+    let seen = List.mem (from, str) !deja_vu_v in
     if not seen then
-      let () = addQueue deja_vu_v str in
-      try
-        let file_str = Hashtbl.find vKnown str in
-        (canonize file_str, !suffixe) :: acc
-      with Not_found -> acc
+      let () = addQueue deja_vu_v (from, str) 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 =
@@ -317,8 +317,8 @@ let treat_coq_file chan =
     | None -> acc
     | Some action ->
       let acc = match action with
-      | Require strl ->
-        List.fold_left mark_v_done acc strl
+      | 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 = file_name s dir in
@@ -340,13 +340,12 @@ let treat_coq_file chan =
         List.fold_left decl acc sl
       | Load str ->
         let str = Filename.basename str in
-        let seen = List.mem [str] !deja_vu_v in
+        let seen = List.mem (None, [str]) !deja_vu_v in
         if not seen then
-          let () = addQueue deja_vu_v [str] in
-          try
-            let file_str = Hashtbl.find vKnown [str] in
-            (canonize file_str, ".v") :: acc
-          with Not_found -> acc
+          let () = addQueue deja_vu_v (None, [str]) in
+          match search_v_known [str] with
+          | None -> acc
+          | Some file_str -> (canonize file_str, ".v") :: acc
         else acc
       | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
       in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 38e454aefb..879da6c588 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -72,9 +72,9 @@ let vAccu   = ref ([] : (string * string) list)
 
 let addQueue q v = q := v :: !q
 
-let safe_hash_add cmp clq q (k,v) =
+let safe_hash_add cmp clq q (k, (v, b)) =
   try
-    let v2 = Hashtbl.find q k in
+    let (v2, _) = Hashtbl.find q k in
     if not (cmp v v2) then
       let rec add_clash = function
           (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
@@ -82,8 +82,8 @@ let safe_hash_add cmp clq q (k,v) =
         | [] -> [(k,[v;v2])] in
       clq := add_clash !clq;
       (* overwrite previous bindings, as coqc does *)
-      Hashtbl.add q k v
-  with Not_found -> Hashtbl.add q k v
+      Hashtbl.add q k (v, b)
+  with Not_found -> Hashtbl.add q k (v, b)
 
 (** Files found in the loadpaths.
     For the ML files, the string is the basename without extension.
@@ -112,9 +112,37 @@ let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
 let add_mllib_known, _, search_mllib_known = mkknown ()
 let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
-let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
+let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t)
+(** The associated boolean is true if this is a root path. *)
 let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
 
+let get_prefix p l =
+  let rec drop_prefix_rec = function
+    | (h1::tp, h2::tl) when h1 = h2 -> drop_prefix_rec (tp,tl)
+    | ([], tl) -> Some tl
+    | _ -> None
+  in
+  drop_prefix_rec (p, l)
+
+exception Found of string
+
+let search_v_known ?from s = match from with
+| None -> fst (Hashtbl.find vKnown s)
+| Some from ->
+  let iter logpath (phys_dir, root) =
+    if root then match get_prefix from logpath with
+    | None -> ()
+    | Some rem ->
+      match get_prefix (List.rev s) (List.rev rem) with
+      | None -> ()
+      | Some _ -> raise (Found phys_dir)
+  in
+  try Hashtbl.iter iter vKnown; raise Not_found
+  with Found s -> s
+
+let search_v_known ?from s =
+  try Some (search_v_known ?from s) with Not_found -> None
+
 let clash_v = ref ([]: (string list * string list) list)
 
 let error_cannot_parse s (i,j) =
@@ -153,9 +181,11 @@ let warning_cannot_open_dir dir =
   eprintf "*** Warning: cannot open %s\n" dir;
   flush stderr
 
-let safe_assoc verbose file k =
+let safe_assoc from verbose file k =
   if verbose && List.mem_assoc k !clash_v then warning_clash file k;
-  Hashtbl.find vKnown k
+  match search_v_known ?from k with
+  | None -> raise Not_found
+  | Some path -> path
 
 let absolute_dir dir =
   let current = Sys.getcwd () in
@@ -299,18 +329,18 @@ let rec traite_fichier_Coq suffixe verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
-    let deja_vu_v = ref ([]: string list list)
+    let deja_vu_v = ref ([]: (string list option * string list) list)
     and deja_vu_ml = ref ([] : string list) in
     try
       while true do
       	let tok = coq_action buf in
 	match tok with
-	  | Require strl ->
+	  | Require (from, strl) ->
 	      List.iter (fun str ->
-		if not (List.mem str !deja_vu_v) then begin
-	          addQueue deja_vu_v str;
+		if not (List.mem (from, str) !deja_vu_v) then begin
+	          addQueue deja_vu_v (from, str);
                   try
-                    let file_str = safe_assoc verbose f str in
+                    let file_str = safe_assoc from verbose f str in
                     printf " %s%s" (canonize file_str) suffixe
                   with Not_found ->
 		    if verbose && not (Hashtbl.mem coqlibKnown str) then
@@ -339,10 +369,10 @@ let rec traite_fichier_Coq suffixe verbose f =
 	      in List.iter decl sl
 	  | Load str ->
 	      let str = Filename.basename str in
-	      if not (List.mem [str] !deja_vu_v) then begin
-	        addQueue deja_vu_v [str];
+	      if not (List.mem (None, [str]) !deja_vu_v) then begin
+	        addQueue deja_vu_v (None, [str]);
                 try
-                  let file_str = Hashtbl.find vKnown [str] in
+                  let (file_str, _) = Hashtbl.find vKnown [str] in
                   let canon = canonize file_str in
                   printf " %s.v" canon;
                   traite_fichier_Coq suffixe true (canon ^ ".v")
@@ -431,9 +461,11 @@ let add_known recur phys_dir log_dir f =
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
-	let paths = if recur then suffixes name else [name] in
-	List.iter
-	  (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths
+	let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
+	if recur then
+          let paths = List.tl (suffixes name) in
+          let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
+          List.iter iter paths
     | (basename,".vo") when not(!option_boot) ->
         let name = log_dir@[basename] in
 	let paths = if recur then suffixes name else [name] in
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 3ac602183f..dcd69ebdb7 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -29,7 +29,7 @@ val iter_mli_known : (string -> dir -> unit) -> unit
 val search_mli_known : string -> dir option
 val add_mllib_known : string -> dir -> string -> unit
 val search_mllib_known : string -> dir option
-val vKnown : (string list, string) Hashtbl.t
+val search_v_known : ?from:string list -> string list -> string option
 val coqlibKnown : (string list, unit) Hashtbl.t
 val file_name : string -> string option -> string
 val escape : string -> string
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index c7b9c9a0a8..84c9ba798b 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -11,7 +11,7 @@ type mL_token = Use_module of string
 type qualid = string list
 
 type coq_token =
-    Require of qualid list
+    Require of qualid option * qualid list
   | Declare of string list
   | Load of string
   | AddLoadPath of string
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 5692e5b45f..291bc55fbe 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -16,7 +16,7 @@
   type qualid = string list
 
   type coq_token =
-    | Require of qualid list
+    | Require of qualid option * qualid list
     | Declare of string list
     | Load of string
     | AddLoadPath of string
@@ -270,12 +270,9 @@ and require_file = parse
         module_names := [coq_qual_id_tail lexbuf];
         let qid = coq_qual_id_list lexbuf in
         parse_dot lexbuf;
-	match !from_pre_ident with
-	  None ->
-          Require qid
-	| Some from ->
-	  (from_pre_ident := None ;
-	   Require (List.map (fun x -> from @ x) qid)) }
+        let from = !from_pre_ident in
+        from_pre_ident := None;
+        Require (from, qid) }
   | eof
       { syntax_error lexbuf }
   | _