diff options
| author | Emilio Jesus Gallego Arias | 2020-02-26 22:54:16 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-04 12:09:55 -0500 |
| commit | 3b9958992cec645f3671aa17d004f035488f222c (patch) | |
| tree | ae9c5abf5cb1b30affa83a629f120b04a8ae1689 /kernel | |
| parent | cfecd54efac7191690f37af1edcc91389ae180e1 (diff) | |
[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.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
