From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 10:26:08 +0200 Subject: Remove some uses of Loadpath.get_paths. The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files. --- library/loadpath.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 26af809e78..d35dca2125 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -112,3 +112,9 @@ let expand_path dir = if DirPath.equal dir lg then (ph, lg) :: aux l else aux l in aux !load_paths + +let locate_file fname = + let paths = get_paths () in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + longfname -- cgit v1.2.3 From b248c23b84a96ef692e4a3ded6668733820e1a77 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 30 Sep 2015 06:52:01 +0200 Subject: Unexport Loadpath.get_paths. --- library/loadpath.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index d35dca2125..622d390a2c 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -28,8 +28,6 @@ let physical p = p.path_physical let get_load_paths () = !load_paths -let get_paths () = List.map physical !load_paths - let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -114,7 +112,7 @@ let expand_path dir = aux !load_paths let locate_file fname = - let paths = get_paths () in + let paths = List.map physical !load_paths in let _,longfname = System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in longfname -- cgit v1.2.3 From d55676344c8dc0d9a87b2ef12ec2348281db4bf5 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 14:10:31 +0100 Subject: Move the From logic to Loadpath.expand_path. --- library/loadpath.ml | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 622d390a2c..16b4194544 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -97,18 +97,19 @@ let filter_path f = in aux !load_paths -let expand_path dir = +let expand_path ?root dir = let rec aux = function | [] -> [] - | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> - match implicit with - | true -> - (** The path is implicit, so that we only want match the logical suffix *) - if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l - | false -> - (** Otherwise we must match exactly *) - if DirPath.equal dir lg then (ph, lg) :: aux l else aux l - in + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then is_dirpath_suffix_of dir lg + else DirPath.equal dir lg + | Some root -> + is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in + if success then (ph, lg) :: aux l else aux l in aux !load_paths let locate_file fname = -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- library/loadpath.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 16b4194544..f77bd1ef53 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit = end | _ -> anomaly_too_many_paths phys_path -let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p - (List.rev_map Id.to_string (DirPath.repr dir)) - let filter_path f = let rec aux = function | [] -> [] -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- library/loadpath.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 622d390a2c..78f8dd25f3 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*