diff options
| -rw-r--r-- | toplevel/coqinit.ml | 35 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 4 |
2 files changed, 26 insertions, 13 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 9faa455657..68db320b9d 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -56,14 +56,21 @@ let build_stdlib_vo_path ~unix_path ~coq_path = let open Loadpath in { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true } +(* Note we don't use has_ml=true due to #12771 , we need to see if we + should just remove that option *) let build_userlib_path ~unix_path = let open Loadpath in - { unix_path - ; coq_path = Libnames.default_root_prefix - ; has_ml = true - ; implicit = false - ; recursive = true - } + if Sys.file_exists unix_path then + let ml_path = System.all_subdirs ~unix_path |> List.map fst in + let vo_path = + { unix_path + ; coq_path = Libnames.default_root_prefix + ; has_ml = false + ; implicit = false + ; recursive = true + } in + ml_path, [vo_path] + else [], [] (* LoadPath for Coq user libraries *) let libs_init_load_path ~coqlib = @@ -75,8 +82,14 @@ let libs_init_load_path ~coqlib = let coq_path = Names.DirPath.make [Libnames.coq_root] in (* ML includes *) - let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") in - List.map fst plugins_dirs, + let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in + + let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in + + let misc_ml, misc_vo = + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in + + plugins_dirs @ contrib_ml @ List.concat misc_ml, (* current directory (not recursively!) *) [ { unix_path = "." @@ -90,9 +103,7 @@ let libs_init_load_path ~coqlib = [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) - (if Sys.file_exists user_contrib then - [build_userlib_path ~unix_path:user_contrib] else [] - ) @ + contrib_vo @ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) - List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) + List.concat misc_vo diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 2bfbbde50e..b96a0ef162 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -14,7 +14,9 @@ val set_debug : unit -> unit val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t -(* LoadPath for Coq user libraries *) +(** Standard LoadPath for Coq user libraries; in particular it + includes (in-order) Coq's standard library, Coq's [user-contrib] + folder, and directories specified in [COQPATH] and [XDG_DIRS] *) val libs_init_load_path : coqlib:CUnix.physical_path -> CUnix.physical_path list * Loadpath.vo_path list |