[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.

1 files changed, 9 insertions, 2 deletions

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. *)