[coqinit] Respect order of ML includes

This fixes a regression introduced in #11618, where I didn't realize
that the order of ML includes would be important as users may want to
shadow it.

In general I do believe that shadowing is tricky and the build system
should handle it, but for now makes sense to preserver the behavior.

The fix is not very nice, but we cannot afford to tweak the API as
this should be backported to 8.12.1; there is a pending PR refactoring
a bit more the toplevel init that should clean this up.

Fixes #12771

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