diff options
| -rw-r--r-- | CHANGES | 10 | ||||
| -rw-r--r-- | library/loadpath.ml | 22 | ||||
| -rw-r--r-- | library/loadpath.mli | 12 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 21 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 21 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 17 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 4 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
10 files changed, 70 insertions, 47 deletions
@@ -15,8 +15,8 @@ Vernacular commands is deprecated. - The coq/user-contrib directory and the XDG directories are no longer recursively added to the load path, so files from installed libraries - now need to be fully qualified for the "Require" command to find - them. The tools/update-require script can be used to convert a development. + now need to be fully qualified for the "Require" command to find them. + The tools/update-require script can be used to convert a development. Notations @@ -97,8 +97,10 @@ Tools - Option -I now only adds directories to the ml path. To add to both the load path and the ml path, use -I -as. -- Option -nois prevents coq/theories and coq/plugins to be recursively - added to the load path. (Same behavior as with coq/user-contrib.) +- Option -Q behaves as -I -as and -R, except that the logical path of + any loaded file has to be fully qualified. +- Option -nois loads coq/theories and coq/plugins as if using -Q rather + than -R. (Same behavior as with coq/user-contrib.) Internal Infrastructure diff --git a/library/loadpath.ml b/library/loadpath.ml index 7c203bc88..2a548fcb6 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -12,12 +12,14 @@ open Errors open Names open Libnames +type path_type = ImplicitPath | ImplicitRootPath | RootPath + (** Load paths. Mapping from physical to logical paths. *) type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_is_root : bool; + path_type : path_type; } let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" @@ -57,18 +59,18 @@ 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 isroot coq_path = +let add_load_path phys_path path_type coq_path = 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_is_root = isroot; + path_type = path_type; } in match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths; - if isroot then + if path_type <> ImplicitPath then accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc) (phys_path :: !accessible_paths) (System.all_subdirs phys_path) | [p] -> @@ -99,7 +101,7 @@ let expand_root_path dir = let rec aux = function | [] -> [] | p :: l -> - if p.path_is_root && is_dirpath_prefix_of p.path_logical dir then + if p.path_type <> ImplicitPath && 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 else aux l @@ -129,9 +131,13 @@ let expand_path dir = let rec aux = function | [] -> [] | p :: l -> - if p.path_is_root then + match p.path_type with + | ImplicitPath -> expand p dir :: aux l + | ImplicitRootPath -> let inters = intersections p.path_logical dir in List.map (expand p) inters @ aux l - else - expand p dir :: aux l in + | RootPath -> + if is_dirpath_prefix_of p.path_logical dir then + expand p (drop_dirpath_prefix p.path_logical dir) :: aux l + else aux l in aux !load_paths diff --git a/library/loadpath.mli b/library/loadpath.mli index f755ace9e..af86122cf 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -15,6 +15,11 @@ open Names *) +type path_type = + | ImplicitPath (** Can be implicitly appended to a logical path. *) + | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *) + | RootPath (** Can only be a prefix of a logical path. *) + type t (** Type of loadpath bindings. *) @@ -33,10 +38,9 @@ val get_paths : unit -> CUnix.physical_path list val get_accessible_paths : unit -> CUnix.physical_path list (** Same as [get_paths] but also get paths that can be relatively accessed. *) -val add_load_path : CUnix.physical_path -> bool -> DirPath.t -> unit -(** [add_load_path root phys log] adds the binding [phys := log] to the current - loadpaths. The [root] flag indicates whether this loadpath has to be treated - as a root one. *) +val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit +(** [add_load_path phys type log] 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, diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 005f6c4ec..85a59c50e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,26 +59,26 @@ let load_rcfile() = (* Puts dir in the path of ML and in the LoadPath *) let coq_add_path unix_path s = - Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]); + Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; Mltop.add_ml_dir unix_path (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = if !Flags.load_init then - Mltop.add_rec_path ~unix_path ~coq_root + Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true else - Mltop.add_path ~unix_path ~coq_root; + Mltop.add_path ~unix_path ~coq_root ~implicit:false; if with_ml then Mltop.add_rec_ml_dir unix_path let add_userlib_path ~unix_path = - Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix; + Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path (* Options -I, -I-as, and -R of the command line *) let includes = ref [] -let push_include (s, alias) = includes := (s,alias,false) :: !includes -let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes +let push_include s alias recursive implicit = + includes := (s,alias,recursive,implicit) :: !includes let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes @@ -104,11 +104,12 @@ let init_load_path () = (* then directories in COQPATH *) List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; (* then current directory *) - Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix; - (* additional loadpath, given with options -I-as and -R *) + Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false; + (* additional loadpath, given with options -I-as, -Q, and -R *) List.iter - (fun (unix_path, coq_root, reci) -> - if reci then Mltop.add_rec_path ~unix_path ~coq_root else Mltop.add_path ~unix_path ~coq_root) + (fun (unix_path, coq_root, reci, implicit) -> + (if reci then Mltop.add_rec_path else Mltop.add_path) + ~unix_path ~coq_root ~implicit) (List.rev !includes); (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 4ca8b61f8..942ef143b 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -15,8 +15,9 @@ val set_rcfile : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit -val push_include : string * Names.DirPath.t -> unit -val push_rec_include : string * Names.DirPath.t -> unit +val push_include : string -> Names.DirPath.t -> bool -> bool -> unit +(** [push_include phys_path log_path recursive implicit] *) + val push_ml_include : string -> unit val init_load_path : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6d92eaa5a..bf0c872cc 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -73,13 +73,11 @@ let outputstate = ref "" let set_outputstate s = outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate -let set_default_include d = push_include (d,Nameops.default_root_prefix) -let set_include d p = +let set_default_include d = + push_include d Nameops.default_root_prefix false false +let set_include d p recursive implicit = let p = dirpath_of_string p in - push_include (d,p) -let set_rec_include d p = - let p = dirpath_of_string p in - push_rec_include(d,p) + push_include d p recursive implicit let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -305,16 +303,21 @@ let parse_args arglist = (* Complex options with many args *) |"-I"|"-include" -> begin match rem with - | d :: "-as" :: p :: rem -> set_include d p; args := rem + | d :: "-as" :: p :: rem -> set_include d p false true; args := rem | d :: "-as" :: [] -> error_missing_arg "-as" | d :: rem -> push_ml_include d; args := rem | [] -> error_missing_arg opt end + |"-Q" -> + begin match rem with + | d :: p :: rem -> set_include d p true false; args := rem + | _ -> error_missing_arg opt + end |"-R" -> begin match rem with - | d :: "-as" :: p :: rem -> set_rec_include d p; args := rem | d :: "-as" :: [] -> error_missing_arg "-as" - | d :: p :: rem -> set_rec_include d p; args := rem + | d :: "-as" :: p :: rem + | d :: p :: rem -> set_include d p true true; args := rem | _ -> error_missing_arg opt end diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index e0cb2209d..458fe8ef0 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -152,11 +152,13 @@ let add_rec_ml_dir unix_path = (* Adding files to Coq and ML loadpath *) -let add_path ~unix_path:dir ~coq_root:coq_dirpath = +let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit = if exists_dir dir then begin add_ml_dir dir; - Loadpath.add_load_path dir true coq_dirpath + Loadpath.add_load_path dir + (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) + coq_dirpath end else msg_warning (str ("Cannot open " ^ dir)) @@ -167,7 +169,7 @@ let convert_string d = msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); raise Exit -let add_rec_path ~unix_path ~coq_root = +let add_rec_path ~unix_path ~coq_root ~implicit = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in let prefix = Names.DirPath.repr coq_root in @@ -180,9 +182,12 @@ let add_rec_path ~unix_path ~coq_root = let dirs = List.map_filter convert_dirs dirs in let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in let () = add_ml_dir unix_path in - let add (path, dir) = Loadpath.add_load_path path false dir in - let () = List.iter add dirs in - Loadpath.add_load_path unix_path true coq_root + let add (path, dir) = + Loadpath.add_load_path path Loadpath.ImplicitPath dir in + let () = if implicit then List.iter add dirs in + Loadpath.add_load_path unix_path + (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) + coq_root else msg_warning (str ("Cannot open " ^ unix_path)) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 1b9257c61..19b999631 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -43,8 +43,8 @@ val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit (** Adds a path to the Coq and ML paths *) -val add_path : unix_path:string -> coq_root:Names.DirPath.t -> unit -val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> unit +val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit +val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 834314094..73a509577 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -20,9 +20,10 @@ let print_usage_channel co command = output_string co " -I dir look for ML files in dir\ \n -include dir (idem)\ -\n -I dir -as coqdir map physical dir to logical coqdir\ +\n -I dir -as coqdir implicitly map physical dir to logical coqdir\ \n -R dir -as coqdir recursively map physical dir to logical coqdir\ \n -R dir coqdir (idem)\ +\n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ \n -notop set the toplevel name to be the empty logical path\ \n -exclude-dir f exclude subdirectories named f for option -R\ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b948a0535..1854e1126 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -857,7 +857,7 @@ let vernac_add_loadpath isrec pdir ldiropt = let pdir = expand pdir in let alias = Option.default Nameops.default_root_prefix ldiropt in (if isrec then Mltop.add_rec_path else Mltop.add_path) - ~unix_path:pdir ~coq_root:alias + ~unix_path:pdir ~coq_root:alias ~implicit:true let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) |