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

1 files changed, 5 insertions, 0 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).