Boot.Env
Rocq runtime enviroment API.
This module provides functions for manipulation of Rocq'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:
It is important that this library has a minimal dependency set.
The Rocq 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:
ROCQLIB
env variable will be used if settheories/Init/Prelude.vo
will be checked, in the following order:coqlibsuffix
given in configurecoqlib
given in configureROCQRUNTIMELIB
env variable is also used if set, if not, the location of the rocq-runtime files will be assumed to be ROCQLIB/../rocq-runtime
, except if ROCQLIB/plugins
exists as in some developers layouts
, in which case we will set ROCQRUNTIMELIB:=ROCQLIB
.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 Rocq'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.
module Path : sig ... end
This API is loosely inspired by Stdune.Path
, for now we keep it minimal, but at some point we may extend it.
val initialized : unit -> maybe_env option
Returns None
if the environment has not been initialized.
val init_with : coqlib:string option -> t
Init, possibly with a user provided coqlib
val maybe_init : warn_ignored_coqlib:(unit -> unit) -> boot:bool ->
coqlib:string option -> maybe_env
Init if boot:false, possibly with a user provided coqlib. Incompatible arguments run warn_ignored_coqlib
(ie with boot:true and coqlib:Some)
val print_queries_maybe_init : warn_ignored_coqlib:(unit -> unit) -> boot:bool ->
coqlib:string option -> Usage.specific_usage option -> Usage.query list -> (maybe_env, string) Stdlib.result
If the query list is empty, behave as maybe_init
. Otherwise, print the queries.
If the usage
argument is None
, the queries must not be PrintHelp.
If a query needs an environment, boot
must not be true
. If there are queries and none need an environment, returns Ok Boot
even if boot
was false
.
val print_config : ?prefix_var_name:string -> t -> Stdlib.out_channel -> unit
val relocate : Coq_config.relocatable_path -> string