Merge PR #13198: [coqinit] Respect order of ML includes

Reviewed-by: herbelin
Ack-by: SkySkimmer

2 files changed, 43 insertions, 28 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 9faa455657..501047c520 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,24 +82,30 @@ 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,
-
-  (* current directory (not recursively!) *)
-  [ { unix_path = "."
-    ; coq_path = Libnames.default_root_prefix
-    ; implicit = false
-    ; has_ml = true
-    ; recursive = false
-    } ] @
-
-  (* then standard library *)
-  [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 []
-  ) @
-
-  (* 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)
+  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
+
+  let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in
+  let vo_loadpath =
+    (* current directory (not recursively!) *)
+    [ { unix_path = "."
+      ; coq_path = Libnames.default_root_prefix
+      ; implicit = false
+      ; has_ml = true
+      ; recursive = false
+      } ] @
+
+    (* then standard library *)
+    [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
+
+    (* then user-contrib *)
+    contrib_vo @
+
+    (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
+    List.concat misc_vo
+  in
+  ml_loadpath, vo_loadpath
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