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. Use warn 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 coqlib : unit -> string

coqlib is the path to the Coq library.

val coqcorelib : unit -> string

coqcorelib is the path to the Coq ML libraries, to be replaced by ocamlfind

val docdir : unit -> string

docdir is the path to the installed documentation.

val datadir : unit -> string

datadir is the path to the installed data directory.

val configdir : unit -> string

configdir is the path to the installed config directory.

val set_coqlib : fail:(string -> string) -> unit

set_coqlib must be run once before any access to coqlib

val set_user_coqlib : string -> unit

set_user_coqlib path sets the coqlib directory explicitedly.

val coqbin : string

coqbin is the name of the current executable.

val coqroot : string

coqroot is the path to coqbin. 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.

val ocamlfind : unit -> string

camlfind () is the path to the ocamlfind binary.

val xdg_config_home : (string -> unit) -> string

Coq tries to honor the XDG Base Directory Specification to access the user's configuration files.

see http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html

val xdg_data_home : (string -> unit) -> string
val xdg_data_dirs : (string -> unit) -> string list
val xdg_dirs : warn:(string -> unit) -> string list
val print_config : ?⁠prefix_var_name:string -> Stdlib.out_channel -> string list -> unit
Prints the configuration information