aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-26 22:54:16 -0500
committerEmilio Jesus Gallego Arias2020-03-04 12:09:55 -0500
commit3b9958992cec645f3671aa17d004f035488f222c (patch)
treeae9c5abf5cb1b30affa83a629f120b04a8ae1689 /kernel
parentcfecd54efac7191690f37af1edcc91389ae180e1 (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