Merge PR #11618: [loadpath] Rework and simplify ML loadpath handling

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes

6 files changed, 43 insertions, 56 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index dceb811d66..f75a706041 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -104,7 +104,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
-  let iload_path = build_load_path opts in
+  let ml_load_path, vo_load_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
   let output_native_objects = match opts.config.native_compiler with
@@ -129,8 +129,8 @@ let compile opts copts ~echo ~f_in ~f_out =
   | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VoDoc long_f_dot_out;
-                iload_path; require_libs; stm_options;
+          Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path;
+                vo_load_path; require_libs; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
@@ -181,8 +181,8 @@ let compile opts copts ~echo ~f_in ~f_out =
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VioDoc long_f_dot_out;
-                iload_path; require_libs; stm_options;
+          Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path;
+                vo_load_path; require_libs; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
@@ -252,8 +252,9 @@ let do_vio opts copts =
   (* We must initialize the loadpath here as the vio scheduling
      process happens outside of the STM *)
   if copts.vio_files <> [] || copts.vio_tasks <> [] then
-    let iload_path = build_load_path opts in
-    List.iter Loadpath.add_coq_path iload_path;
+    let ml_lp, vo_lp = build_load_path opts in
+    List.iter Mltop.add_ml_dir ml_lp;
+    List.iter Loadpath.add_vo_path vo_lp;
 
   (* Vio compile pass *)
   if copts.vio_files <> [] then schedule_vio copts;
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 949a13974c..24cfecd057 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -70,8 +70,8 @@ type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
 
-  ml_includes : Loadpath.coq_path list;
-  vo_includes : Loadpath.coq_path list;
+  ml_includes : string list;
+  vo_includes : Loadpath.vo_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -164,14 +164,13 @@ let default = {
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }}
+  { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
 
 let add_vo_include opts unix_path coq_path implicit =
   let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
   { opts with pre = { opts.pre with vo_includes = {
-        recursive = true;
-        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }}
+        unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
   { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
@@ -582,9 +581,7 @@ let prelude_data = "Prelude", Some "Coq", Some false
 let require_libs opts =
   if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
-let cmdline_load_path opts =
-  opts.pre.ml_includes @ opts.pre.vo_includes
-
 let build_load_path opts =
-  (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @
-  cmdline_load_path opts
+  let ml_path, vo_path = if opts.pre.boot then [],[] else Coqinit.libs_init_load_path () in
+  ml_path @ opts.pre.ml_includes ,
+  vo_path @ opts.pre.vo_includes
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index aba6811f43..88de48967a 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -46,8 +46,8 @@ type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
 
-  ml_includes : Loadpath.coq_path list;
-  vo_includes : Loadpath.coq_path list;
+  ml_includes : CUnix.physical_path list;
+  vo_includes : Loadpath.vo_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -83,4 +83,4 @@ val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * strin
 val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
-val build_load_path : t -> Loadpath.coq_path list
+val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7f3d4b570f..ce054d2af2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -51,34 +51,22 @@ let load_rcfile ~rcfile ~state =
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
 
-(* Recursively puts `.v` files in the LoadPath if -nois was not passed *)
+(* Recursively puts `.v` files in the LoadPath *)
 let build_stdlib_vo_path ~unix_path ~coq_path =
   let open Loadpath in
-  { recursive = true;
-    path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true }
-  }
-
-let build_stdlib_ml_path ~dir =
-  let open Loadpath in
-  { recursive = true
-  ; path_spec = MlPath dir
-  }
+  { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
 
 let build_userlib_path ~unix_path =
   let open Loadpath in
-  { recursive = true;
-    path_spec = VoPath {
-        unix_path;
-        coq_path = Libnames.default_root_prefix;
-        has_ml = AddRecML;
-        implicit = false;
-      }
+  { unix_path
+  ; coq_path = Libnames.default_root_prefix
+  ; has_ml = true
+  ; implicit = false
+  ; recursive = true
   }
 
 let ml_path_if c p =
-  let open Loadpath in
-  let f x = { recursive = false; path_spec = MlPath x } in
-  if c then List.map f p else []
+  if c then p else []
 
 (* LoadPath for developers *)
 let toplevel_init_load_path () =
@@ -97,16 +85,19 @@ let libs_init_load_path () =
   let coqpath = Envars.coqpath in
   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!) *)
-  [ { recursive = false;
-      path_spec = VoPath { unix_path = ".";
-                           coq_path = Libnames.default_root_prefix;
-                           implicit = false;
-                           has_ml = AddTopML }
+  [ { unix_path = "."
+    ; coq_path = Libnames.default_root_prefix
+    ; implicit = false
+    ; has_ml = true
+    ; recursive = false
     } ] @
 
   (* then standard library *)
-  [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @
   [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
 
   (* then user-contrib *)
@@ -120,10 +111,8 @@ let libs_init_load_path () =
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
-  let open Loadpath in
-  let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Loadpath.add_coq_path (lp (List.fold_left (/) (Envars.coqlib()) [dl]))
+    Mltop.add_ml_dir (List.fold_left (/) (Envars.coqlib()) [dl])
   in
-    Loadpath.add_coq_path (lp (Envars.coqlib ()));
-    List.iter add_subdir Coq_config.all_src_dirs
+  Mltop.add_ml_dir (Envars.coqlib ());
+  List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index f3a007d987..f099173808 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State
 val init_ocaml_path : unit -> unit
 
 (* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> Loadpath.coq_path list
+val toplevel_init_load_path : unit -> CUnix.physical_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : unit -> Loadpath.coq_path list
+val libs_init_load_path : unit -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1ea48ee766..1e6b1023fe 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -226,7 +226,7 @@ let init_execution opts custom_init =
   Spawned.init_channels ();
   if opts.post.memory_stat then at_exit print_memory_stat;
   let top_lp = Coqinit.toplevel_init_load_path () in
-  List.iter Loadpath.add_coq_path top_lp;
+  List.iter Mltop.add_ml_dir top_lp;
   CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
   (* Configuration *)
@@ -281,14 +281,14 @@ let init_document opts =
   *)
   (* Next line allows loading .vos files when in interactive mode *)
   Flags.load_vos_libraries := true;
-  let iload_path = build_load_path opts in
+  let ml_load_path, vo_load_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
            { doc_type = Interactive opts.config.logic.toplevel_name;
-             iload_path; require_libs; stm_options;
+             ml_load_path; vo_load_path; require_libs; stm_options;
            }) in
   { doc; sid; proof = None; time = opts.config.time }