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 ssubstitutes 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- warnas a message displayer.
- val home : warn:(string -> unit) -> string
- home warnreturns 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,- warnis called.
- val set_coqlib : fail:(string -> string) -> unit
- set_coqlibmust be run once before any access to- coqlib
- val coqroot : string
- coqrootis 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
- coqpathis 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.