[init] Add `-boot` option to avoid binding `Coq.` prefix.

This is useful when we want to have finer control of the location of
files in the bootstrap process, for example when building using Dune.

Also, this makes options consistent with what `coqdep` already uses
for bootstrap.

The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust.

Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.

6 files changed, 17 insertions, 7 deletions

diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst
new file mode 100644
index 0000000000..49dd0ee2d8
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the
+  `Coq` library prefix by default
+  (`#11617 <https://github.com/coq/coq/pull/11617>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 506a8dc5b0..2b79bff1b2 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -64,6 +64,7 @@ type coqargs_config = {
 }
 
 type coqargs_pre = {
+  boot        : bool;
   load_init   : bool;
   load_rcfile : bool;
 
@@ -131,6 +132,7 @@ let default_config = {
 }
 
 let default_pre = {
+  boot         = false;
   load_init    = true;
   load_rcfile  = true;
   ml_includes  = [];
@@ -512,6 +514,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
+    |"-boot" -> { oval with pre = { oval.pre with boot = true }}
     |"-output-context" -> { oval with post = { oval.post with output_context = true }}
     |"-profile-ltac" -> Flags.profile_ltac := true; oval
     |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
@@ -569,5 +572,5 @@ let cmdline_load_path opts =
   opts.pre.ml_includes @ opts.pre.vo_includes
 
 let build_load_path opts =
-  Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
+  (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @
   cmdline_load_path opts
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 26f22386a0..f38381a086 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -40,6 +40,7 @@ type coqargs_config = {
 }
 
 type coqargs_pre = {
+  boot        : bool;
   load_init   : bool;
   load_rcfile : bool;
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3aa9acfc52..7f3d4b570f 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -52,10 +52,10 @@ let load_rcfile ~rcfile ~state =
       iraise reraise
 
 (* Recursively puts `.v` files in the LoadPath if -nois was not passed *)
-let build_stdlib_vo_path ~load_init ~unix_path ~coq_path =
+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 = load_init }
+    path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true }
   }
 
 let build_stdlib_ml_path ~dir =
@@ -88,7 +88,7 @@ let toplevel_init_load_path () =
   ml_path_if Coq_config.local [coqlib/"dev"]
 
 (* LoadPath for Coq user libraries *)
-let libs_init_load_path ~load_init =
+let libs_init_load_path () =
 
   let open Loadpath in
   let coqlib = Envars.coqlib () in
@@ -107,7 +107,7 @@ let libs_init_load_path ~load_init =
 
   (* then standard library *)
   [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @
-  [build_stdlib_vo_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path] @
+  [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
 
   (* then user-contrib *)
   (if Sys.file_exists user_contrib then
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index fc53c8b47c..f3a007d987 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -20,4 +20,4 @@ val init_ocaml_path : unit -> unit
 val toplevel_init_load_path : unit -> Loadpath.coq_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : load_init:bool -> Loadpath.coq_path list
+val libs_init_load_path : unit -> Loadpath.coq_path list
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 6848862603..ba3deeb2f6 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -32,7 +32,8 @@ let print_usage_common co command =
 \n  -coqlib dir            set the coq standard library directory\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
-\n  -noinit                start without loading the Init library\
+\n  -boot                  don't bind the `Coq.` prefix to the default -coqlib dir\
+\n  -noinit                don't load Coq.Init.Prelude on start \
 \n  -nois                  (idem)\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
 \n\