From 7489014fa6053c28e09852b0bf0602f2160cdda5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 16 Feb 2020 17:54:14 -0500
Subject: [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.
---
 toplevel/usage.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'toplevel/usage.ml')

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\
-- 
cgit v1.2.3