Module Boot.EnvSource

Coq runtime enviroment API.

This module provides functions for manipulation of Coq's runtime enviroment, including the standard directories and support files.

This API is similar in spirit to findlib's or dune-sites API, see their documentation for more information:

• http://projects.camlcity.org/projects/dl/findlib-1.9.1/doc/ref-html/lib/index.html
• https://dune.readthedocs.io/en/stable/sites.html#sites

It is important that this library has a minimal dependency set.

The Coq runtime enviroment needs to be properly initialized before use; we detail the rules below. It is recommended that applications requiring multiple accesses to the environment, do initialize it once and keep a ref to it. We don't forbid yet double initialization, (second time is a noop) but we may do so in the future. Rules for "coqlib" are:

• the COQLIB env variable will be used if set
• if not, the existence of theories/Init/Prelude.vo will be checked, in the following order:

1. coqlibsuffix given in configure
2. coqlib given in configure

• if none of the above succeeds, the initialization will fail

• The COQCORELIB env variable is also used if set, if not, the location of the coq-core files will be assumed to be COQLIB/../coq-core, except if COQLIB/plugins exists as in some developers layouts, in which case we will set COQCORELIB:=COQLIB.

Note that set_coqlib is used by some commands to process the -coqlib option, as of now this sets both coqlib and coqcorelib; this part of the initialization will be eventually moved here.

The error handling policy of this module is simple for now: failing to initialize Coq's env will produce a fatal error, and the application will exit with code 1. No error handling is thus required on the client yet.