diff --git a/doc/changelog/09-cli-tools/18165-br-coqdep-fix.rst b/doc/changelog/09-cli-tools/18165-br-coqdep-fix.rst new file mode 100644 index 000000000000..f841d589c106 --- /dev/null +++ b/doc/changelog/09-cli-tools/18165-br-coqdep-fix.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Spurious `coqdep` warnings due to missing path normalization for plugins + (`#18165 `_, + by Rodolphe Lepigre). diff --git a/tools/coqdep/lib/file_util.ml b/tools/coqdep/lib/file_util.ml new file mode 100644 index 000000000000..17d8622d78b7 --- /dev/null +++ b/tools/coqdep/lib/file_util.ml @@ -0,0 +1,38 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* string = fun full_path -> + if Filename.is_relative full_path then full_path else + let cwd = String.split_on_char '/' (Sys.getcwd ()) in + let path = String.split_on_char '/' full_path in + let rec remove_common_prefix l1 l2 = + match (l1, l2) with + | (x1 :: l1, x2 :: l2) when x1 = x2 -> remove_common_prefix l1 l2 + | (_ , _ ) -> (l1, String.concat "/" l2) + in + let (cwd, path) = remove_common_prefix cwd path in + let add_parent path _ = Filename.concat Filename.parent_dir_name path in + List.fold_left add_parent path cwd + +let normalize_path : string -> string = fun path -> + let re_delim = if Sys.win32 then "[/\\]" else "/" in + let path = Str.split_delim (Str.regexp re_delim) path in + let rec normalize acc path = + match (path, acc) with + | ([] , _ ) -> List.rev acc + | ("." :: path, _ ) -> normalize acc path + | (".." :: path, [] ) -> normalize (".." :: []) path + | (".." :: path, ".." :: _ ) -> normalize (".." :: acc) path + | (".." :: path, _ :: acc) -> normalize acc path + | (dir :: path, _ ) -> normalize (dir :: acc) path + in + match normalize [] path with + | [] -> "." + | path -> String.concat "/" path diff --git a/tools/coqdep/lib/file_util.mli b/tools/coqdep/lib/file_util.mli new file mode 100644 index 000000000000..260cb6a8ba15 --- /dev/null +++ b/tools/coqdep/lib/file_util.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* string + +(** [normalize_path path] takes as input a file path [path], and returns an + equivalent path that: (1) does not contain the current directory member + ["."] unless the path is to the current directory (in which case ["."] + is returned, or ["./"] if [path] has a trailing ["/"]), (2) only uses + parent directory members [".."] for a prefix of the path, and (3), has + a trailing ["/"] only if and only if [path] does. + + For example, paths ["dir1/dir2/file.v"], ["."], ["dir1/dir2/dir3/"] and + ["../../dir/file.v"] are possible return values, but ["./file.v"] and + ["dir1/../dir2"] are not. *) +val normalize_path : string -> string diff --git a/tools/coqdep/lib/fl.ml b/tools/coqdep/lib/fl.ml index 8e5871523822..8052362755f3 100644 --- a/tools/coqdep/lib/fl.ml +++ b/tools/coqdep/lib/fl.ml @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open File_util + module Error = struct exception CannotFindMeta of string * string @@ -86,48 +88,6 @@ let rec find_plugin meta_file plugin_name path p { Fl_metascanner.pkg_defs ; pkg let path = path @ [find_plugin_field "directory" "." c.Fl_metascanner.pkg_defs] in find_plugin meta_file plugin_name path ps c -(** [to_relative_path path] takes as input a file path [path], and constructs - an equivalent relative path from the current working directory. If [path] - is already relative, then it is returned immediately. *) -let to_relative_path : string -> string = fun full_path -> - if Filename.is_relative full_path then full_path else - let cwd = String.split_on_char '/' (Sys.getcwd ()) in - let path = String.split_on_char '/' full_path in - let rec remove_common_prefix l1 l2 = - match (l1, l2) with - | (x1 :: l1, x2 :: l2) when x1 = x2 -> remove_common_prefix l1 l2 - | (_ , _ ) -> (l1, String.concat "/" l2) - in - let (cwd, path) = remove_common_prefix cwd path in - let add_parent path _ = Filename.concat Filename.parent_dir_name path in - List.fold_left add_parent path cwd - -(** [normalize_path path] takes as input a file path [path], and returns an - equivalent path that: (1) does not contain the current directory member - ["."] unless the path is to the current directory (in which case ["."] - is returned, or ["./"] if [path] has a trailing ["/"]), (2) only uses - parent directory members [".."] for a prefix of the path, and (3), has - a trailing ["/"] only if and only if [path] does. - - For example, paths ["dir1/dir2/file.v"], ["."], ["dir1/dir2/dir3/"] and - ["../../dir/file.v"] are possible return values, but ["./file.v"] and - ["dir1/../dir2"] are not. *) -let normalize_path : string -> string = fun path -> - let re_delim = if Sys.win32 then "[/\\]" else "/" in - let path = Str.split_delim (Str.regexp re_delim) path in - let rec normalize acc path = - match (path, acc) with - | ([] , _ ) -> List.rev acc - | ("." :: path, _ ) -> normalize acc path - | (".." :: path, [] ) -> normalize (".." :: []) path - | (".." :: path, ".." :: _ ) -> normalize (".." :: acc) path - | (".." :: path, _ :: acc) -> normalize acc path - | (dir :: path, _ ) -> normalize (dir :: acc) path - in - match normalize [] path with - | [] -> "." - | path -> String.concat "/" path - let findlib_resolve ~meta_files ~file ~package ~plugin_name = let (meta_file, meta) = match find_parsable_META meta_files package with diff --git a/tools/coqdep/lib/loadpath.ml b/tools/coqdep/lib/loadpath.ml index 36b3ae85dbea..d4c48a77075d 100644 --- a/tools/coqdep/lib/loadpath.ml +++ b/tools/coqdep/lib/loadpath.ml @@ -193,6 +193,7 @@ module State = struct } let gen_add h x s suff = + let s = Option.map File_util.normalize_path s in try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff with Not_found -> Hashtbl.add h x (s,suff)