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. --- doc/changelog/07-commands-and-options/11617-toplevel+boot.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/11617-toplevel+boot.rst (limited to 'doc') 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 `_, + by Emilio Jesus Gallego Arias). -- cgit v1.2.3