[boot] Don't initialize coqlib when `-boot` is passed.

We refactor handling of `-boot` so the "coqlib" guessing routine,
`Envars.coqlib ()` is not called when bootstrapping.

In compositional builds involving Coq's prelude we don't want for this
guessing to happen, as the heuristics to locate the prelude will fail
due to different build layout choices.

Thus after this patch Coq does not do any guessing when `-boot` is
passed, leaving the location of libraries to the usual command line
parameters.

Note that some other tooling still calls `Envars.coqlib`, however this
should happen late enough as for it to be safe; we will fix that
eventually when we consolidate the library for library handling among
tools.

Ideally, we would also remove `Envars.coqlib` altogether, as we want
to avoid clients accessing the Coq filesystem in a non-controlled way.

5 files changed, 28 insertions, 41 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 24cfecd057..ef97e57a5c 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -582,6 +582,10 @@ let require_libs opts =
   if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
 let build_load_path opts =
-  let ml_path, vo_path = if opts.pre.boot then [],[] else Coqinit.libs_init_load_path () in
+  let ml_path, vo_path =
+    if opts.pre.boot then [],[]
+    else
+      let coqlib = Envars.coqlib () in
+      Coqinit.libs_init_load_path ~coqlib in
   ml_path @ opts.pre.ml_includes ,
   vo_path @ opts.pre.vo_includes
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index f6b173968f..4041d02953 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -65,21 +65,10 @@ let build_userlib_path ~unix_path =
   ; recursive = true
   }
 
-let ml_path_if c p =
-  if c then p else []
-
-(* LoadPath for developers *)
-let toplevel_init_load_path () =
-  let coqlib = Envars.coqlib () in
-  (* NOTE: These directories are searched from last to first *)
-  (* first, developer specific directory to open *)
-  ml_path_if Coq_config.local [coqlib/"dev"]
-
 (* LoadPath for Coq user libraries *)
-let libs_init_load_path () =
+let libs_init_load_path ~coqlib =
 
   let open Loadpath 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
@@ -107,12 +96,3 @@ let libs_init_load_path () =
 
   (* 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)
-
-(* Initialises the Ocaml toplevel before launching it, so that it can
-   find the "include" file in the *source* directory *)
-let init_ocaml_path () =
-  let add_subdir dl =
-    Mltop.add_ml_dir (List.fold_left (/) (Envars.coqlib()) [dl])
-  in
-  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 f099173808..eb6b37000e 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -14,10 +14,7 @@ val set_debug : unit -> unit
 
 val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
 
-val init_ocaml_path : unit -> unit
-
-(* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> CUnix.physical_path list
-
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : unit -> CUnix.physical_path list * Loadpath.vo_path list
+val libs_init_load_path
+  : coqlib:CUnix.physical_path
+  -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b0012f8978..7ff58039d4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -501,10 +501,16 @@ let rec vernac_loop ~state =
   let state, drop = read_and_execute ~state in
   if drop then state else vernac_loop ~state
 
-(* Default toplevel loop *)
+(* Default toplevel loop, machinery for drop is below *)
 
 let drop_args = ref None
 
+(* Initialises the Ocaml toplevel before launching it, so that it can
+   find the "include" file in the *source* directory *)
+let init_ocaml_path ~coqlib =
+  let add_subdir dl = Mltop.add_ml_dir (Filename.concat coqlib dl) in
+  List.iter add_subdir ("dev" :: Coq_config.all_src_dirs)
+
 let loop ~opts ~state =
   drop_args := Some opts;
   let open Coqargs in
@@ -517,7 +523,8 @@ let loop ~opts ~state =
   (* Call the main loop *)
   let _ : Vernac.State.t = vernac_loop ~state in
   (* Initialise and launch the Ocaml toplevel *)
-  Coqinit.init_ocaml_path();
+  let coqlib = Envars.coqlib () in
+  init_ocaml_path ~coqlib;
   Mltop.ocaml_toploop();
   (* We delete the feeder after the OCaml toploop has ended so users
      of Drop can see the feedback. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1e6b1023fe..876388092d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -155,19 +155,22 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
-let init_setup = function
-  | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
-  | Some s -> Envars.set_user_coqlib s
+let init_coqlib opts = match opts.config.coqlib with
+  | None when opts.pre.boot -> ()
+  | None ->
+    Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+  | Some s ->
+    Envars.set_user_coqlib s
 
 let print_query opts = function
   | PrintVersion -> Usage.version ()
   | PrintMachineReadableVersion -> Usage.machine_readable_version ()
   | PrintWhere ->
-    let () = init_setup opts.config.coqlib in
+    let () = init_coqlib opts in
     print_endline (Envars.coqlib ())
   | PrintHelp h -> Usage.print_usage stderr h
   | PrintConfig ->
-    let () = init_setup opts.config.coqlib in
+    let () = init_coqlib opts in
     Envars.print_config stdout Coq_config.all_src_dirs
   | PrintTags -> print_style_tags opts.config
 
@@ -217,16 +220,12 @@ let init_parse parse_extra help init_opts =
     end;
   opts, customopts
 
+(** Coq's init process, phase 2: Basic Coq environment, plugins. *)
 let init_execution opts custom_init =
-  (* Coq's init process, phase 2:
-     Basic Coq environment, load-path, plugins.
-   *)
   (* If we have been spawned by the Spawn module, this has to be done
    * early since the master waits us to connect back *)
   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 Mltop.add_ml_dir top_lp;
   CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
   (* Configuration *)
@@ -268,7 +267,7 @@ let init_toplevel custom =
   match opts.main with
   | Queries q -> List.iter (print_query opts) q; exit 0
   | Run ->
-    let () = init_setup opts.config.coqlib in
+    let () = init_coqlib opts in
     let customstate = init_execution opts (custom.init customopts) in
     opts, customopts, customstate