Merge PR coq#19124: [loadpath] Export pure version of `try_locate_abs…

…olute_library` Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <[email protected]>
SkySkimmer · Jun 4, 2024 · edd043e · edd043e
2 parents 344c7b4 + 6c7c826
commit edd043e
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 9 deletions.
diff --git a/dev/ci/user-overlays/19124-ejgallego-export_locate_result.sh 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
@@ -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
@@ -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 } *)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		overlay tactician https://github.com/ejgallego/coq-tactician export_locate_result 19124