From 6735186e6458fedd57efd663c900166af0d6fce3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 29 Jun 2008 16:24:36 +0000 Subject: Lissage de la gestion des chemins de chargement de fichiers : - Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.ml | 2 + library/libnames.mli | 1 + library/library.ml | 104 ++++++++++++++++++++++++++++++++++----------------- library/library.mli | 8 ++-- library/states.ml | 4 +- 5 files changed, 81 insertions(+), 38 deletions(-) (limited to 'library') diff --git a/library/libnames.ml b/library/libnames.ml index dfa0fb82d..04ab34baa 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -89,6 +89,8 @@ let drop_dirpath_prefix d1 d2 = let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in make_dirpath (List.rev d) +let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1) + (* To know how qualified a name should be to be understood in the current env*) let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) diff --git a/library/libnames.mli b/library/libnames.mli index fe5033d73..890a442e3 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -59,6 +59,7 @@ val chop_dirpath : int -> dir_path -> dir_path * dir_path val drop_dirpath_prefix : dir_path -> dir_path -> dir_path val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool +val append_dirpath : dir_path -> dir_path -> dir_path module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path diff --git a/library/library.ml b/library/library.ml index 272f01f7d..b17be690a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -24,9 +24,9 @@ open Nametab type logical_path = dir_path -let load_paths = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([] : (System.physical_path * logical_path * bool) list) -let get_load_paths () = fst !load_paths +let get_load_paths () = List.map pi1 !load_paths (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = @@ -56,12 +56,12 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p -let find_logical_path phys_dir = +let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in - match list_filter2 (fun p d -> p = phys_dir) !load_paths with - | _,[dir] -> dir - | _,[] -> Nameops.default_root_prefix - | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) + match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with + | [_,dir,_] -> dir + | [] -> Nameops.default_root_prefix + | l -> anomaly ("Two logical paths are associated to "^phys_dir) let is_in_load_paths phys_dir = let dir = canonical_path_name phys_dir in @@ -70,12 +70,12 @@ let is_in_load_paths phys_dir = List.exists check_p lp let remove_load_path dir = - load_paths := list_filter2 (fun p d -> p <> dir) !load_paths + load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths -let add_load_path (phys_path,coq_path) = +let add_load_path isroot (phys_path,coq_path) = let phys_path = canonical_path_name phys_path in - match list_filter2 (fun p d -> p = phys_path) !load_paths with - | _,[dir] -> + match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with + | [_,dir,_] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not @@ -90,18 +90,54 @@ let add_load_path (phys_path,coq_path) = pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); remove_load_path phys_path; - load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) + load_paths := (phys_path,coq_path,isroot) :: !load_paths; end - | _,[] -> - load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) + | [] -> + load_paths := (phys_path,coq_path,isroot) :: !load_paths; | _ -> anomaly ("Two logical paths are associated to "^phys_path) let physical_paths (dp,lp) = dp -let load_paths_of_dir_path dir = - fst (list_filter2 (fun p d -> d = dir) !load_paths) - -let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) +let extend_path_with_dirpath p dir = + List.fold_left Filename.concat p + (List.map string_of_id (List.rev (repr_dirpath dir))) + +let root_paths_matching_dir_path dir = + let rec aux = function + | [] -> [] + | (p,d,true) :: l when is_dirpath_prefix_of d dir -> + let suffix = drop_dirpath_prefix d dir in + extend_path_with_dirpath p suffix :: aux l + | _ :: l -> 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 d1 = empty_dirpath 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 loadpaths_matching_dir_path dir = + let rec aux = function + | [] -> [] + | (p,d,true) :: l -> + let inters = intersections d dir in + List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl)) + inters @ + aux l + | (p,d,_) :: l -> + (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in + aux !load_paths + +let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (************************************************************************) (*s Modules on disk contain the following informations (after the magic @@ -196,6 +232,12 @@ let library_full_filename dir = try LibraryFilenameMap.find dir !libraries_filename_table with Not_found -> "" +let overwrite_library_filenames f = + let f = + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in + LibraryMap.iter (fun dir _ -> register_library_filename dir f) + !libraries_table + let library_is_loaded dir = try let _ = find_library dir in true with Not_found -> false @@ -334,11 +376,11 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = load_paths_of_dir_path pref in + let loadpath = root_paths_matching_dir_path pref in if loadpath = [] then raise LibUnmappedDir; try let name = (string_of_id base)^".vo" in - let _, file = System.where_in_path loadpath name in + let _, file = System.where_in_path false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -347,20 +389,15 @@ let locate_absolute_library dir = else raise LibNotFound -let locate_qualified_library qid = +let locate_qualified_library warn qid = try (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = - if repr_dirpath dir = [] then get_load_paths () - else - (* we assume dir is an absolute dirpath *) - load_paths_of_dir_path dir - in + let dir, base = repr_qualid qid in + let loadpath = loadpaths_matching_dir_path dir in if loadpath = [] then raise LibUnmappedDir; - let name = (string_of_id base)^".vo" in - let path, file = System.where_in_path loadpath name in - let dir = extend_dirpath (find_logical_path path) base in + let name = string_of_id base ^ ".vo" in + let lpath, file = System.where_in_path warn (List.map fst loadpath) name in + let dir = extend_dirpath (List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -386,7 +423,7 @@ let try_locate_absolute_library dir = let try_locate_qualified_library (loc,qid) = try - let (_,dir,f) = locate_qualified_library qid in + let (_,dir,f) = locate_qualified_library true qid in dir,f with e -> explain_locate_library_error qid e @@ -586,8 +623,7 @@ let import_module export (loc,qid) = (*s Initializing the compilation of a library. *) let start_library f = - let _,longf = - System.find_file_in_path (get_load_paths ()) (f^".v") in + let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in let ldir = extend_dirpath ldir0 id in diff --git a/library/library.mli b/library/library.mli index 1e2197409..d7cef3243 100644 --- a/library/library.mli +++ b/library/library.mli @@ -52,6 +52,9 @@ val opened_libraries : unit -> dir_path list (* - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string + (* - Overwrite the filename of all libraries (used when restoring a state) *) +val overwrite_library_filenames : string -> unit + (*s Hook for the xml exportation of libraries *) val set_xml_require : (dir_path -> unit) -> unit @@ -61,11 +64,10 @@ val set_xml_require : (dir_path -> unit) -> unit val get_load_paths : unit -> System.physical_path list val get_full_load_paths : unit -> (System.physical_path * dir_path) list -val add_load_path : System.physical_path * dir_path -> unit +val add_load_path : bool -> System.physical_path * dir_path -> unit val remove_load_path : System.physical_path -> unit val find_logical_path : System.physical_path -> dir_path val is_in_load_paths : System.physical_path -> bool -val load_paths_of_dir_path : dir_path -> System.physical_path list (*s Locate a library in the load paths *) exception LibUnmappedDir @@ -73,7 +75,7 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - qualid -> library_location * dir_path * System.physical_path + bool -> qualid -> library_location * dir_path * System.physical_path (*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds diff --git a/library/states.ml b/library/states.ml index dcb4111ed..7c3953151 100644 --- a/library/states.ml +++ b/library/states.ml @@ -24,7 +24,9 @@ let state_magic_number = 19764 let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in (fun s -> raw_extern s (freeze())), - (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s)) + (fun s -> + unfreeze (raw_intern (Library.get_load_paths ()) s); + Library.overwrite_library_filenames s) (* Rollback. *) -- cgit v1.2.3