From 6c7c826d9e3380477a97069ac4c1c1009e971b69 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 31 May 2024 17:22:37 +0200 Subject: [PATCH] [loadpath] Export pure version of `try_locate_absolute_library` This is from my coq-lsp share-require branch, and would be nice to have for the 8.20 version. --- .../19124-ejgallego-export_locate_result.sh | 1 + vernac/loadpath.ml | 13 +++++++------ vernac/loadpath.mli | 10 +++++++--- 3 files changed, 15 insertions(+), 9 deletions(-) create mode 100644 dev/ci/user-overlays/19124-ejgallego-export_locate_result.sh diff --git a/dev/ci/user-overlays/19124-ejgallego-export_locate_result.sh b/dev/ci/user-overlays/19124-ejgallego-export_locate_result.sh new file mode 100644 index 000000000000..d92033d6a23a --- /dev/null +++ b/dev/ci/user-overlays/19124-ejgallego-export_locate_result.sh @@ -0,0 +1 @@ +overlay tactician https://github.com/ejgallego/coq-tactician export_locate_result 19124 diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 74f4de47f3c7..b159c3e7909e 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -176,8 +176,9 @@ let locate_file fname = (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) -type locate_error = LibUnmappedDir | LibNotFound -type 'a locate_result = ('a, locate_error) result +module Error = struct + type t = LibUnmappedDir | LibNotFound +end (* If [!Flags.load_vos_libraries] and the .vos file exists @@ -190,7 +191,7 @@ let select_vo_file ~find base = let name = Names.Id.to_string base ^ ext in let lpath, file = find name in Ok (lpath, file) - with Not_found -> Error LibNotFound in + with Not_found -> Error Error.LibNotFound in if !Flags.load_vos_libraries then begin match find ".vos" with @@ -212,7 +213,7 @@ let find_unique fullqid loadpath base = CErrors.user_err Pp.(str "Required library " ++ Libnames.pr_qualid fullqid ++ strbrk " matches several files in path (found " ++ pr_enum str (List.map snd l) ++ str ").") -let locate_absolute_library dir : CUnix.physical_path locate_result = +let locate_absolute_library dir : (CUnix.physical_path, Error.t) Result.t = (* Search in loadpath *) let pref, base = Libnames.split_dirpath dir in let loadpath = filter_path (fun dir -> DP.equal dir pref) in @@ -224,7 +225,7 @@ let locate_absolute_library dir : CUnix.physical_path locate_result = | Error fail -> Error fail let locate_qualified_library ?root qid : - (DP.t * CUnix.physical_path) locate_result = + (DP.t * CUnix.physical_path, Error.t) Result.t = (* Search library in loadpath *) let dir, base = Libnames.repr_qualid qid in match expand_path ?root dir with @@ -237,7 +238,7 @@ let locate_qualified_library ?root qid : | Error _ -> (* Looking otherwise in -R/-Q blocks of partial matches *) let rec aux = function - | [] -> Error LibUnmappedDir + | [] -> Error Error.LibUnmappedDir | block :: rest -> match select_vo_file ~find:(find_unique qid block) base with | Ok _ as x -> x diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index bc986eec8e61..d515f94ea5a6 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -52,13 +52,14 @@ val locate_file : string -> string it does not respect the visibility of paths. *) (** {6 Locate a library in the load path } *) -type locate_error = LibUnmappedDir | LibNotFound -type 'a locate_result = ('a, locate_error) result +module Error : sig + type t = LibUnmappedDir | LibNotFound +end val locate_qualified_library : ?root:DirPath.t -> Libnames.qualid - -> (DirPath.t * CUnix.physical_path) locate_result + -> (DirPath.t * CUnix.physical_path, Error.t) Result.t (** Locates a library by implicit name. @@ -67,7 +68,10 @@ val locate_qualified_library *) +val locate_absolute_library : DirPath.t -> (CUnix.physical_path, Error.t) Result.t + val try_locate_absolute_library : DirPath.t -> string +(* To do in another PR: [@@deprecated "use locate_absolute_library instead"] *) (** {6 Extending the Load Path } *)