[stm] [toplevel] Make loadpath a parameter of the document.

We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.

The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:

- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
  command line options, etc...

3 files changed, 44 insertions, 20 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b3b5375bf..10205964a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -89,22 +89,26 @@ let ml_path_if c p =
   let f x = { recursive = false; path_spec = MlPath x } in
   if c then List.map f p else []
 
-(* Initializes the LoadPath *)
-let init_load_path ~load_init =
-  let open Mltop in
+(* LoadPath for toploop toplevels *)
+let toplevel_init_load_path () =
   let coqlib = Envars.coqlib () in
-  let user_contrib = coqlib/"user-contrib" in
-  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
-  let coqpath = Envars.coqpath in
-  let coq_path = Names.DirPath.make [Libnames.coq_root] in
-
   (* NOTE: These directories are searched from last to first *)
   (* first, developer specific directory to open *)
   ml_path_if Coq_config.local [coqlib/"dev"] @
 
   (* main loops *)
   ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @
-  ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] @
+  ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"]
+
+(* LoadPath for Coq user libraries *)
+let libs_init_load_path ~load_init =
+
+  let open Mltop in
+  let coqlib = Envars.coqlib () in
+  let user_contrib = coqlib/"user-contrib" in
+  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
+  let coqpath = Envars.coqpath in
+  let coq_path = Names.DirPath.make [Libnames.coq_root] in
 
   (* then standard library and plugins *)
   [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false;
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 089847f5d..0d2da84bb 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -19,5 +19,10 @@ val push_include : string -> Names.DirPath.t -> bool -> unit
 (** [push_include phys_path log_path implicit] *)
 
 val push_ml_include : string -> unit
-val init_load_path : load_init:bool -> Mltop.coq_path list
+
 val init_ocaml_path : unit -> unit
+
+(* LoadPath for toploop toplevels *)
+val toplevel_init_load_path : unit ->  Mltop.coq_path list
+(* LoadPath for Coq user libraries *)
+val libs_init_load_path : load_init:bool -> Mltop.coq_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index bf090862f..400f7048d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -304,6 +304,9 @@ let compile ~time ~verbosely ~f_in ~f_out =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
+  let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+  let require_libs = require_libs () in
+  let stm_options = !top_stm_options in
   match !compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
@@ -316,8 +319,9 @@ let compile ~time ~verbosely ~f_in ~f_out =
 
       let doc, sid = Stm.(new_doc
           { doc_type = VoDoc long_f_dot_vo;
-            require_libs = require_libs ();
-            stm_options = !top_stm_options;
+            iload_path;
+            require_libs;
+            stm_options;
           }) in
 
       let doc, sid = load_init_vernaculars ~time doc sid in
@@ -352,8 +356,9 @@ let compile ~time ~verbosely ~f_in ~f_out =
 
       let doc, sid = Stm.(new_doc
           { doc_type = VioDoc long_f_dot_vio;
-            require_libs = require_libs ();
-            stm_options = !top_stm_options;
+            iload_path;
+            require_libs;
+            stm_options;
           }) in
 
       let doc, sid = load_init_vernaculars ~time doc sid in
@@ -424,7 +429,12 @@ let set_vio_checking_j opt j =
     prerr_endline "setting the J variable like in 'make vio2vo J=3'";
     exit 1
 
-let schedule_vio opts =
+let schedule_vio () =
+  (* We must add update the loadpath here as the scheduling process
+     happens outside of the STM *)
+  let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+  List.iter Mltop.add_coq_path iload_path;
+
   if !vio_checking then
     Vio_checking.schedule_vio_checking !vio_files_j !vio_files
   else
@@ -494,7 +504,8 @@ let usage batch =
     try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
     with NoCoqLib -> usage_no_coqlib ()
   end;
-  let lp = Coqinit.init_load_path ~load_init:!load_init in
+  let lp = Coqinit.toplevel_init_load_path () in
+  (* Necessary for finding the toplevels below *)
   List.iter Mltop.add_coq_path lp;
   if batch then Usage.print_usage_coqc ()
   else begin
@@ -808,8 +819,8 @@ let init_toplevel arglist =
       if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
       if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
-      let lp = Coqinit.init_load_path ~load_init:!load_init in
-      List.iter Mltop.add_coq_path lp;
+      let top_lp = Coqinit.toplevel_init_load_path () in
+      List.iter Mltop.add_coq_path top_lp;
       Option.iter Mltop.load_ml_object_raw !toploop;
       let extras = !toploop_init extras in
       if not (CList.is_empty extras) then begin
@@ -845,11 +856,15 @@ let init_toplevel arglist =
           || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks))
       (* Interactive *)
       then begin
+        let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+        let require_libs = require_libs () in
+        let stm_options = !top_stm_options in
         try
           let doc, sid = Stm.(new_doc
                                 { doc_type = Interactive !toplevel_name;
-                                  require_libs = require_libs ();
-                                  stm_options = !top_stm_options;
+                                  iload_path;
+                                  require_libs;
+                                  stm_options;
                                 }) in
           Some (load_init_vernaculars ~time:!measure_time doc sid)
         with any -> flush_all(); fatal_error any