From 765510929b2255d9c56fcdfce4a3ea555b07b340 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 Mar 2015 18:25:45 +0200 Subject: A more reasonable implementation of Loadpath. The new behaviour is simple: either a path is in the loadpaths or it is not. No more wild expansions of paths! This should not affect -R and -Q, but it does change the semantics of -I -as. Still, there are no more users of it and it only does so in a subtle way. --- library/loadpath.ml | 48 ++++++++++++++---------------------------------- 1 file changed, 14 insertions(+), 34 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index ab8b0a3078..0f7c2fb465 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -93,47 +93,27 @@ let expand_root_path dir = let rec aux = function | [] -> [] | p :: l -> - if p.path_root && is_dirpath_prefix_of p.path_logical dir then - let suffix = drop_dirpath_prefix p.path_logical dir in - extend_path_with_dirpath p.path_physical suffix :: aux l + if DirPath.equal p.path_logical dir then p.path_physical :: aux l else aux l in aux !load_paths -(* Root p is bound to A.B.C.D and we require file C.D.E.F *) -(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) - -(* Root p is bound to A.B.C.C and we require file C.C.E.F *) -(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) - -let intersections d1 d2 = - let rec aux d1 = - if DirPath.is_empty d1 then [d2] else - let rest = aux (snd (chop_dirpath 1 d1)) in - if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest - else rest in - aux d1 - -let expand p dir = - let ph = extend_path_with_dirpath p.path_physical dir in - let log = append_dirpath p.path_logical dir in - (ph, log) +let is_suffix dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 let expand_path dir = let rec aux = function | [] -> [] | p :: l -> - match p.path_implicit, p.path_root with - | true, false -> expand p dir :: aux l - | true, true -> - let inters = intersections p.path_logical dir in - List.map (expand p) inters @ aux l - | false, true -> - if is_dirpath_prefix_of p.path_logical dir then - expand p (drop_dirpath_prefix p.path_logical dir) :: aux l - else aux l - | false, false -> - (* nothing to do, an explicit root path should also match above - if [is_dirpath_prefix_of p.path_logical dir] were true here *) - aux l in + let { path_physical = ph; path_logical = lg } = p in + match p.path_implicit with + | true -> + (** The path is implicit, so that we only want match the logical suffix *) + if is_suffix 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 aux !load_paths -- cgit v1.2.3 From 43a0a3147073b12b038c55c27fd6f0adcb900ac9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 Mar 2015 19:24:10 +0200 Subject: Removing the unused root flag from loadpaths. --- 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 0f7c2fb465..ca22801021 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -17,7 +17,6 @@ open Libnames type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_root : bool; path_implicit : bool; } @@ -53,13 +52,12 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path coq_path ~root ~implicit = +let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in let binding = { path_logical = coq_path; path_physical = phys_path; - path_root = root; path_implicit = implicit; } in match List.filter filter !load_paths with -- cgit v1.2.3 From 7c41bc9bdc883aacbc015954a89ff13fe9c9c1c0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 Apr 2015 10:51:32 +0200 Subject: From X Require Y looks for X with absolute path, disregarding -R. --- library/loadpath.ml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index ca22801021..54ea0be4f9 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -87,20 +87,15 @@ let extend_path_with_dirpath p dir = List.fold_left Filename.concat p (List.rev_map Id.to_string (DirPath.repr dir)) -let expand_root_path dir = +let filter_path f = let rec aux = function | [] -> [] | p :: l -> - if DirPath.equal p.path_logical dir then p.path_physical :: aux l + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l else aux l in aux !load_paths -let is_suffix dir1 dir2 = - let dir1 = DirPath.repr dir1 in - let dir2 = DirPath.repr dir2 in - List.prefix_of Id.equal dir1 dir2 - let expand_path dir = let rec aux = function | [] -> [] @@ -109,7 +104,7 @@ let expand_path dir = match p.path_implicit with | true -> (** The path is implicit, so that we only want match the logical suffix *) - if is_suffix dir lg then (ph, lg) :: aux l else aux l + 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 -- cgit v1.2.3 From 049f329908ab6702c3a933ddc45ae6b6f5160065 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 2 Apr 2015 13:36:43 +0200 Subject: Make it possible for -R to override the existing implicit setting of a path. Without this commit, passing "-R theories Coq" to "coqtop -nois" has no effect since "-Q theories Coq" has already been done implicitly. --- library/loadpath.ml | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 54ea0be4f9..26af809e78 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -63,21 +63,24 @@ let add_load_path phys_path coq_path ~implicit = match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths - | [p] -> - let dir = p.path_logical in - if not (DirPath.equal coq_path dir) - (* If this is not the default -I . to coqtop *) - && not - (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && DirPath.equal coq_path (Nameops.default_root_prefix)) - then + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else if DirPath.equal coq_path (Nameops.default_root_prefix) + && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then + false (* This is the default "-I ." path, don't override the old path *) + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Nameops.default_root_prefix) then + msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) in + true in + if replace then begin - (* Assume the user is concerned by library naming *) - if not (DirPath.equal dir Nameops.default_root_prefix) then - msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); remove_load_path phys_path; load_paths := binding :: !load_paths; end @@ -99,9 +102,8 @@ let filter_path f = let expand_path dir = let rec aux = function | [] -> [] - | p :: l -> - let { path_physical = ph; path_logical = lg } = p in - match p.path_implicit with + | { 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 -- cgit v1.2.3