diff options
| -rw-r--r-- | dev/ci/user-overlays/09895-ejgallego-require+upper.sh | 6 | ||||
| -rw-r--r-- | library/library.ml | 103 | ||||
| -rw-r--r-- | library/library.mli | 27 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | library/loadpath.ml | 119 | ||||
| -rw-r--r-- | stm/stm.ml | 4 | ||||
| -rw-r--r-- | stm/stm.mli | 2 | ||||
| -rw-r--r-- | toplevel/ccompile.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 10 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 6 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 16 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | vernac/loadpath.ml | 273 | ||||
| -rw-r--r-- | vernac/loadpath.mli (renamed from library/loadpath.mli) | 68 | ||||
| -rw-r--r-- | vernac/mltop.ml | 72 | ||||
| -rw-r--r-- | vernac/mltop.mli | 24 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 41 |
19 files changed, 399 insertions, 382 deletions
diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh new file mode 100644 index 0000000000..9a42c829ce --- /dev/null +++ b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then + + quickchick_CI_REF=require+upper + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/library/library.ml b/library/library.ml index d8eaf5f659..9f4eb531ed 100644 --- a/library/library.ml +++ b/library/library.ml @@ -264,85 +264,6 @@ let in_import_library : DirPath.t list * bool -> obj = subst_function = subst_import_library; classify_function = classify_import_library } - -(************************************************************************) -(*s Locate absolute or partially qualified library names in the path *) - -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -let warn_several_object_files = - CWarnings.create ~name:"several-object-files" ~category:"require" - (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ - strbrk " instead of " ++ str vo ++ - strbrk " because it is more recent") - -let locate_absolute_library dir = - (* Search in loadpath *) - let pref, base = split_dirpath dir in - let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let loadpath = List.map fst loadpath in - let find ext = - try - let name = Id.to_string base ^ ext in - let _, file = System.where_in_path ~warn:false loadpath name in - Some file - with Not_found -> None in - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some file, None | None, Some file -> file - | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - vi - | Some vo, Some _ -> vo - -let locate_qualified_library ?root ?(warn = true) qid = - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path ?root dir in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let find ext = - try - let name = Id.to_string base ^ ext in - let lpath, file = - System.where_in_path ~warn (List.map fst loadpath) name in - Some (lpath, file) - with Not_found -> None in - let lpath, file = - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some res, None | None, Some res -> res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - resvi - | Some resvo, Some _ -> resvo - in - let dir = add_dirpath_suffix (String.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 *) - else (LibInPath, dir, file) - -let error_unmapped_dir qid = - let prefix, _ = repr_qualid qid in - user_err ~hdr:"load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) - -let error_lib_not_found qid = - user_err ~hdr:"load_absolute_library_from" - (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") - -let try_locate_absolute_library dir = - try - locate_absolute_library dir - with - | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) - | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) - (************************************************************************) (** {6 Tables of opaque proof terms} *) @@ -450,7 +371,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let rec intern_library (needed, contents) (dir, f) from = +let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -459,7 +380,7 @@ let rec intern_library (needed, contents) (dir, f) from = with Not_found -> Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let f = match f with Some f -> f | None -> try_locate_absolute_library dir in + let f = match f with Some f -> f | None -> lib_resolver dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then user_err ~hdr:"load_physical_library" @@ -467,22 +388,24 @@ let rec intern_library (needed, contents) (dir, f) from = DirPath.print m.library_name ++ spc () ++ str "and not library" ++ spc() ++ DirPath.print dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m f + m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f -and intern_library_deps libs dir m from = - let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in +and intern_library_deps ~lib_resolver libs dir m from = + let needed, contents = + Array.fold_left (intern_mandatory_library ~lib_resolver dir from) + libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) -and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) (Some from) in +and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = + let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then user_err (str "Compiled library " ++ DirPath.print caller ++ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ over library " ++ DirPath.print dir); libs -let rec_intern_library libs (dir, f) = - let _, libs = intern_library libs (dir, Some f) None in +let rec_intern_library ~lib_resolver libs (dir, f) = + let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in libs let native_name_from_filename f = @@ -557,8 +480,8 @@ let warn_require_in_module = strbrk "You can Require a module at toplevel " ++ strbrk "and optionally Import it inside another one.") -let require_library_from_dirpath modrefl export = - let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in +let require_library_from_dirpath ~lib_resolver modrefl export = + let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then diff --git a/library/library.mli b/library/library.mli index 390299bf56..f3186d847f 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,11 @@ open Libnames (** {6 ... } Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) -val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit +val require_library_from_dirpath + : lib_resolver:(DirPath.t -> CUnix.physical_path) + -> (DirPath.t * string) list + -> bool option + -> unit (** {6 Start the compilation of a library } *) @@ -45,8 +49,10 @@ val save_library_to : output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit -val load_library_todo : - string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val load_library_todo + : CUnix.physical_path + -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) @@ -65,20 +71,5 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(** {6 Locate a library in the load paths } *) -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -val locate_qualified_library : - ?root:DirPath.t -> ?warn:bool -> qualid -> - library_location * DirPath.t * CUnix.physical_path -(** Locates a library by implicit name. - - @raise LibUnmappedDir if the library is not in the path - @raise LibNotFound if there is no corresponding file in the path - -*) - (** {6 Native compiler. } *) val native_name_from_filename : string -> string diff --git a/library/library.mllib b/library/library.mllib index 8f694f4a31..ef53471377 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -7,7 +7,6 @@ Global Decl_kinds Lib Declaremods -Loadpath Library States Kindops diff --git a/library/loadpath.ml b/library/loadpath.ml deleted file mode 100644 index fc13c864d0..0000000000 --- a/library/loadpath.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Util -open CErrors -open Names -open Libnames - -(** Load paths. Mapping from physical to logical paths. *) - -type t = { - path_physical : CUnix.physical_path; - path_logical : DirPath.t; - path_implicit : bool; -} - -let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" - -let logical p = p.path_logical - -let physical p = p.path_physical - -let get_load_paths () = !load_paths - -let anomaly_too_many_paths path = - anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") - -let find_load_path phys_dir = - let phys_dir = CUnix.canonical_path_name phys_dir in - let filter p = String.equal p.path_physical phys_dir in - let paths = List.filter filter !load_paths in - match paths with - | [] -> raise Not_found - | [p] -> p - | _ -> anomaly_too_many_paths phys_dir - -let is_in_load_paths phys_dir = - let dir = CUnix.canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p p = String.equal dir p.path_physical in - List.exists check_p lp - -let remove_load_path dir = - let filter p = not (String.equal p.path_physical dir) in - load_paths := List.filter filter !load_paths - -let warn_overriding_logical_loadpath = - CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" - (fun (phys_path, old_path, coq_path) -> - str phys_path ++ strbrk " was previously bound to " ++ - DirPath.print old_path ++ strbrk "; it is remapped to " ++ - DirPath.print coq_path) - -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_implicit = implicit; - } in - match List.filter filter !load_paths with - | [] -> - load_paths := binding :: !load_paths - | [{ path_logical = old_path; path_implicit = old_implicit }] -> - let replace = - if DirPath.equal coq_path old_path then - implicit <> old_implicit - else - let () = - (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Libnames.default_root_prefix) then - warn_overriding_logical_loadpath (phys_path, old_path, coq_path) - in - true in - if replace then - begin - remove_load_path phys_path; - load_paths := binding :: !load_paths; - end - | _ -> anomaly_too_many_paths phys_path - -let filter_path f = - let rec aux = function - | [] -> [] - | p :: l -> - if f p.path_logical then (p.path_physical, p.path_logical) :: aux l - else aux l - in - aux !load_paths - -let expand_path ?root dir = - let rec aux = function - | [] -> [] - | { 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 = - let paths = List.map physical !load_paths in - let _,longfname = - System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in - longfname diff --git a/stm/stm.ml b/stm/stm.ml index fc539b5208..d469994f3f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2670,7 +2670,7 @@ type stm_init_options = { (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -2728,7 +2728,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; diff --git a/stm/stm.mli b/stm/stm.mli index a0bbe05b3a..24c672c973 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -69,7 +69,7 @@ type stm_init_options = { (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 2f63410761..7748134146 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -225,7 +225,7 @@ let do_vio opts copts = process happens outside of the STM *) if copts.vio_files <> [] || copts.vio_tasks <> [] then let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; (* Vio compile pass *) if copts.vio_files <> [] then schedule_vio copts; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index ec43dbb1d7..4ef31c73b7 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -46,8 +46,8 @@ type t = { load_rcfile : bool; rcfile : string option; - ml_includes : Mltop.coq_path list; - vo_includes : Mltop.coq_path list; + ml_includes : Loadpath.coq_path list; + vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -147,10 +147,10 @@ let default = { (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } + Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } let add_vo_include opts unix_path coq_path implicit = - let open Mltop in + let open Loadpath in let coq_path = Libnames.dirpath_of_string coq_path in { opts with vo_includes = { recursive = true; @@ -273,7 +273,7 @@ let usage help = end; let lp = Coqinit.toplevel_init_load_path () in (* Necessary for finding the toplevels below *) - List.iter Mltop.add_coq_path lp; + List.iter Loadpath.add_coq_path lp; help () (* Main parsing routine *) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index d7f9819bee..015789c1f3 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -22,8 +22,8 @@ type t = { load_rcfile : bool; rcfile : string option; - ml_includes : Mltop.coq_path list; - vo_includes : Mltop.coq_path list; + ml_includes : Loadpath.coq_path list; + vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; toplevel_name : Stm.interactive_top; @@ -69,4 +69,4 @@ val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list val exitcode : t -> int val require_libs : t -> (string * string option * bool option) list -val build_load_path : t -> Mltop.coq_path list +val build_load_path : t -> Loadpath.coq_path list diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 74a089510e..cbe353004e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -53,25 +53,25 @@ let load_rcfile ~rcfile ~state = (* Recursively puts dir in the LoadPath if -nois was not passed *) let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = - let open Mltop in + let open Loadpath in let add_ml = if with_ml then AddRecML else AddNoML in { recursive = true; path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } } let build_userlib_path ~unix_path = - let open Mltop in + let open Loadpath in { recursive = true; path_spec = VoPath { unix_path; coq_path = Libnames.default_root_prefix; - has_ml = Mltop.AddRecML; + has_ml = AddRecML; implicit = false; } } let ml_path_if c p = - let open Mltop in + let open Loadpath in let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] @@ -85,7 +85,7 @@ let toplevel_init_load_path () = (* LoadPath for Coq user libraries *) let libs_init_load_path ~load_init = - let open Mltop in + let open Loadpath in let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in @@ -115,10 +115,10 @@ let libs_init_load_path ~load_init = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let open Mltop in + let open Loadpath in let lp s = { recursive = false; path_spec = MlPath s } in let add_subdir dl = - Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) + Loadpath.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) in - Mltop.add_coq_path (lp (Envars.coqlib ())); + Loadpath.add_coq_path (lp (Envars.coqlib ())); List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c891e736b4..04ec77a025 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Mltop.coq_path list +val toplevel_init_load_path : unit -> Loadpath.coq_path list (* LoadPath for Coq user libraries *) -val libs_init_load_path : load_init:bool -> Mltop.coq_path list +val libs_init_load_path : load_init:bool -> Loadpath.coq_path list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b769405cf6..460c2f126e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -222,7 +222,7 @@ let init_toplevel ~help ~init custom_init arglist = exit 0; end; let top_lp = Coqinit.toplevel_init_load_path () in - List.iter Mltop.add_coq_path top_lp; + List.iter Loadpath.add_coq_path top_lp; let opts, extras = custom_init ~opts extras in Mltop.init_known_plugins (); diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml new file mode 100644 index 0000000000..1bb44d0ef1 --- /dev/null +++ b/vernac/loadpath.ml @@ -0,0 +1,273 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +module DP = Names.DirPath + +(** Load paths. Mapping from physical to logical paths. *) + +type t = { + path_physical : CUnix.physical_path; + path_logical : DP.t; + path_implicit : bool; +} + +let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" + +let logical p = p.path_logical +let physical p = p.path_physical + +let pp p = + let dir = DP.print p.path_logical in + let path = Pp.str (CUnix.escaped_string_of_physical_path p.path_physical) in + Pp.(hov 2 (dir ++ spc () ++ path)) + +let get_load_paths () = !load_paths + +let anomaly_too_many_paths path = + CErrors.anomaly Pp.(str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") + +let find_load_path phys_dir = + let phys_dir = CUnix.canonical_path_name phys_dir in + let filter p = String.equal p.path_physical phys_dir in + let paths = List.filter filter !load_paths in + match paths with + | [] -> raise Not_found + | [p] -> p + | _ -> anomaly_too_many_paths phys_dir + +let remove_load_path dir = + let filter p = not (String.equal p.path_physical dir) in + load_paths := List.filter filter !load_paths + +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + Pp.(seq [str phys_path; strbrk " was previously bound to " + ; DP.print old_path; strbrk "; it is remapped to " + ; DP.print coq_path])) + +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_implicit = implicit; + } in + match List.filter filter !load_paths with + | [] -> + load_paths := binding :: !load_paths + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DP.equal coq_path old_path then + implicit <> old_implicit + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DP.equal old_path Libnames.default_root_prefix) then + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in + true in + if replace then + begin + remove_load_path phys_path; + load_paths := binding :: !load_paths; + end + | _ -> anomaly_too_many_paths phys_path + +let filter_path f = + let rec aux = function + | [] -> [] + | p :: l -> + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l + else aux l + in + aux !load_paths + +let expand_path ?root dir = + let rec aux = function + | [] -> [] + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then Libnames.is_dirpath_suffix_of dir lg + else DP.equal dir lg + | Some root -> + Libnames.(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 = + let paths = List.map physical !load_paths in + let _,longfname = + System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in + longfname + +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) + +type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + Pp.(fun (vi, vo) -> + seq [ str "Loading"; spc (); str vi + ; strbrk " instead of "; str vo + ; strbrk " because it is more recent" + ]) + + +let select_vo_file ~warn loadpath base = + let find ext = + let loadpath = List.map fst loadpath in + try + let name = Names.Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn loadpath name in + Some (lpath, file) + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + +let locate_absolute_library dir : CUnix.physical_path locate_result = + (* Search in loadpath *) + let pref, base = Libnames.split_dirpath dir in + let loadpath = filter_path (fun dir -> DP.equal dir pref) in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + match select_vo_file ~warn:false loadpath base with + | Ok (_, file) -> Ok file + | Error fail -> Error fail + +let locate_qualified_library ?root ?(warn = true) qid : + (library_location * DP.t * CUnix.physical_path) locate_result = + (* Search library in loadpath *) + let dir, base = Libnames.repr_qualid qid in + let loadpath = expand_path ?root dir in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + match select_vo_file ~warn loadpath base with + | Ok (lpath, file) -> + let dir = Libnames.add_dirpath_suffix + (CString.List.assoc lpath loadpath) base in + (* Look if loaded *) + if Library.library_is_loaded dir + then Ok (LibLoaded, dir, Library.library_full_filename dir) + (* Otherwise, look for it in the file system *) + else Ok (LibInPath, dir, file) + | Error fail -> Error fail + +let error_unmapped_dir qid = + let prefix, _ = Libnames.repr_qualid qid in + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot load "; Libnames.pr_qualid qid; str ":"; spc () + ; str "no physical path bound to"; spc () + ; DP.print prefix; fnl () + ]) + +let error_lib_not_found qid = + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) + +let try_locate_absolute_library dir = + match locate_absolute_library dir with + | Ok res -> res + | Error LibUnmappedDir -> + error_unmapped_dir (Libnames.qualid_of_dirpath dir) + | Error LibNotFound -> + error_lib_not_found (Libnames.qualid_of_dirpath dir) + +(** { 5 Extending the load path } *) + +(* Adds a path to the Coq and ML paths *) +type add_ml = AddNoML | AddTopML | AddRecML + +type vo_path_spec = { + unix_path : string; (* Filesystem path contaning vo/ml files *) + coq_path : DP.t; (* Coq prefix for the path *) + implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> Pp.(str "Cannot open " ++ str unix_path)) + +let warn_cannot_use_directory = + CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" + (fun d -> + Pp.(str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)")) + +let convert_string d = + try Names.Id.of_string d + with + | CErrors.UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in + warn_cannot_use_directory d; + raise Exit + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in + if System.exists_dir unix_path then + let dirs = if recursive then System.all_subdirs ~unix_path else [] in + let prefix = DP.repr lp.coq_path in + let convert_dirs (lp, cp) = + try + let path = List.rev_map convert_string cp @ prefix in + Some (lp, DP.make path) + with Exit -> None + in + let dirs = List.map_filter convert_dirs dirs in + let add_ml_dir = Mltop.add_ml_dir ~recursive:false in + let () = match lp.has_ml with + | AddNoML -> () + | AddTopML -> + Mltop.add_ml_dir ~recursive:false unix_path + | AddRecML -> + List.iter (fun (lp,_) -> add_ml_dir lp) dirs; + add_ml_dir unix_path in + let add (path, dir) = add_load_path path ~implicit dir in + let () = List.iter add dirs in + add_load_path unix_path ~implicit lp.coq_path + else + warn_cannot_open_path unix_path + +let add_coq_path { recursive; path_spec } = match path_spec with + | VoPath lp -> + add_vo_path ~recursive lp + | MlPath dir -> + Mltop.add_ml_dir ~recursive dir diff --git a/library/loadpath.mli b/vernac/loadpath.mli index 4044ca1127..d393fc35b5 100644 --- a/library/loadpath.mli +++ b/vernac/loadpath.mli @@ -20,19 +20,15 @@ open Names type t (** Type of loadpath bindings. *) -val physical : t -> CUnix.physical_path -(** Get the physical path (filesystem location) of a loadpath. *) - val logical : t -> DirPath.t (** Get the logical path (Coq module hierarchy) of a loadpath. *) +val pp : t -> Pp.t +(** Print a load path *) + val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit -(** [add_load_path phys log type] adds the binding [phys := log] to the current - loadpaths. *) - val remove_load_path : CUnix.physical_path -> unit (** Remove the current logical path binding associated to a given physical path, if any. *) @@ -41,17 +37,53 @@ val find_load_path : CUnix.physical_path -> t (** Get the binding associated to a physical path. Raises [Not_found] if there is none. *) -val is_in_load_paths : CUnix.physical_path -> bool -(** Whether a physical path is currently bound. *) - -val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list -(** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible matches of it. *) - -val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list -(** As {!expand_path} but uses a filter function instead, and ignores the - implicit status of loadpaths. *) - val locate_file : string -> string (** Locate a file among the registered paths. Do not use this function, as it does not respect the visibility of paths. *) + +(** {6 Locate a library in the load path } *) +type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +val locate_qualified_library + : ?root:DirPath.t + -> ?warn:bool + -> Libnames.qualid + -> (library_location * DirPath.t * CUnix.physical_path) locate_result + +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) + +val try_locate_absolute_library : DirPath.t -> string + +(** {6 Extending the Load Path } *) + +(** Adds a path to the Coq and ML paths *) +type add_ml = AddNoML | AddTopML | AddRecML + +type vo_path_spec = { + unix_path : string; + (** Filesystem path contaning vo/ml files *) + coq_path : Names.DirPath.t; + (** Coq prefix for the path *) + implicit : bool; + (** [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; + (** If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +val add_coq_path : coq_path -> unit diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 78e26c65d4..bbee9988d0 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -159,75 +159,9 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path (-R) *) -let add_rec_ml_dir unix_path = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) - -(* Adding files to Coq and ML loadpath *) - -let warn_cannot_use_directory = - CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" - (fun d -> - str "Directory " ++ str d ++ - strbrk " cannot be used as a Coq identifier (skipped)") - -let convert_string d = - try Names.Id.of_string d - with UserError _ -> - let d = Unicode.escaped_if_non_utf8 d in - warn_cannot_use_directory d; - raise Exit - -let warn_cannot_open_path = - CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" - (fun unix_path -> str "Cannot open " ++ str unix_path) - -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; - coq_path : Names.DirPath.t; - implicit : bool; - has_ml : add_ml; -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} - -let add_vo_path ~recursive lp = - let unix_path = lp.unix_path in - let implicit = lp.implicit in - if exists_dir unix_path then - let dirs = if recursive then all_subdirs ~unix_path else [] in - let prefix = Names.DirPath.repr lp.coq_path in - let convert_dirs (lp, cp) = - try - let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.DirPath.make path) - with Exit -> None - in - let dirs = List.map_filter convert_dirs dirs in - let () = match lp.has_ml with - | AddNoML -> () - | AddTopML -> add_ml_dir unix_path - | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in - let add (path, dir) = - Loadpath.add_load_path path ~implicit dir in - let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~implicit lp.coq_path - else - warn_cannot_open_path unix_path - -let add_coq_path { recursive; path_spec } = match path_spec with - | VoPath lp -> - add_vo_path ~recursive lp - | MlPath dir -> - if recursive then add_rec_ml_dir dir else add_ml_dir dir +let add_ml_dir ~recursive unix_path = + let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in + List.iter (fun (lp,_) -> add_ml_dir lp) dirs (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 3d796aa4aa..b457c9c88f 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -32,6 +32,9 @@ val ocaml_toploop : unit -> unit (** {5 ML Dynlink} *) +(** Adds a dir to the plugin search path *) +val add_ml_dir : recursive:bool -> string -> unit + (** Tests if we can load ML files *) val has_dynlink : bool @@ -41,27 +44,6 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; (* Filesystem path contaning vo/ml files *) - coq_path : Names.DirPath.t; (* Coq prefix for the path *) - implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} - -val add_coq_path : coq_path -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7f5c265eea..57c56a58f9 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -32,6 +32,7 @@ Assumptions Vernacstate Mltop Topfmt +Loadpath Vernacentries Misctypes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 828356d31d..b9d1326ba5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -201,11 +201,6 @@ let show_match id = (* "Print" commands *) -let print_path_entry p = - let dir = DirPath.print (Loadpath.logical p) in - let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in - Pp.hov 2 (dir ++ spc () ++ path) - let print_loadpath dir = let l = Loadpath.get_load_paths () in let l = match dir with @@ -215,7 +210,7 @@ let print_loadpath dir = List.filter filter l in str "Logical Path / Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l + prlist_with_sep fnl Loadpath.pp l let print_modules () = let opened = Library.opened_libraries () @@ -444,9 +439,9 @@ let locate_file f = str file let msg_found_library = function - | Library.LibLoaded, fulldir, file -> + | Loadpath.LibLoaded, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) - | Library.LibInPath, fulldir, file -> + | Loadpath.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?from qid = @@ -471,10 +466,11 @@ let err_notfound_library ?from qid = (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library qid = - try msg_found_library (Library.locate_qualified_library ~warn:false qid) - with - | Library.LibUnmappedDir -> err_unmapped_library qid - | Library.LibNotFound -> err_notfound_library qid + let open Loadpath in + match locate_qualified_library ~warn:false qid with + | Ok lib -> msg_found_library lib + | Error LibUnmappedDir -> err_unmapped_library qid + | Error LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -1026,18 +1022,18 @@ let vernac_require from import qidl = Some (Libnames.add_dirpath_suffix hd tl) in let locate qid = - try - let warn = not !Flags.quiet in - let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in - (dir, f) - with - | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid - | Library.LibNotFound -> err_notfound_library ?from:root qid + let open Loadpath in + let warn = not !Flags.quiet in + match locate_qualified_library ?root ~warn qid with + | Ok (_,dir,f) -> dir, f + | Error LibUnmappedDir -> err_unmapped_library ?from:root qid + | Error LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun {CAst.loc} dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); - Library.require_library_from_dirpath modrefl import + let lib_resolver = Loadpath.try_locate_absolute_library in + Library.require_library_from_dirpath ~lib_resolver modrefl import (* Coercions and canonical structures *) @@ -1133,7 +1129,7 @@ let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = - let open Mltop in + let open Loadpath in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in add_coq_path { recursive = true; @@ -1141,11 +1137,10 @@ let vernac_add_loadpath implicit pdir ldiropt = let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) - (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - let open Mltop in + let open Loadpath in add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~local l = |