Module Envars
This file provides a high-level interface to the environment variables needed by Coq to run (such as coqlib). The values of these variables may come from different sources (shell environment variables, command line options, options set at the time Coq was build).
val expand_path_macros : warn:(string -> unit) -> string -> string
expand_path_macros warn s
substitutes environment variables in a string by their values. This function also takes care of substituting path of the form '~X' by an absolute path. Usewarn
as a message displayer.
val home : warn:(string -> unit) -> string
home warn
returns the root of the user directory, depending on the OS. This information is usually stored in the $HOME environment variable on POSIX shells. If no such variable exists, then other common names are tried (HOMEDRIVE, HOMEPATH, USERPROFILE). If all of them fail,warn
is called.
val set_coqlib : fail:(string -> string) -> unit
set_coqlib
must be run once before any access tocoqlib
val coqroot : string
coqroot
is the path tocoqbin
. The following value only makes sense when executables are running from source tree (e.g. during build or in local mode).
val coqpath : string list
coqpath
is the standard path to coq. Notice that coqpath is stored in reverse order, since that is the order it gets added to the search path.