package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.lib/Envars/index.html

Module EnvarsSource

This file provides a high-level interface to the environment variables needed by Rocq 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 Rocq was build).

Sourceval getenv_rocq : string -> string option

getenv_rocq name returns the value of "ROCQ$name" if it exists, otherwise the value of "COQ$name" if it exists and warns that it is deprecated, otherwise None.

Sourceval 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.

Sourceval 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.

Sourceval docdir : unit -> string

docdir is the path to the installed documentation.

Sourceval datadir : unit -> string

datadir is the path to the installed data directory.

Sourceval configdir : unit -> string

configdir is the path to the installed config directory.

Sourceval coqbin : string

coqbin is the name of the current executable.

Sourceval 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).

Sourceval 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.

Sourceval ocamlfind : unit -> string

camlfind () is the path to the ocamlfind binary.

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

Rocq 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

Sourceval xdg_data_home : (string -> unit) -> string
Sourceval xdg_data_dirs : (string -> unit) -> string list
Sourceval xdg_dirs : warn:(string -> unit) -> string list
Sourceval print_config : ?prefix_var_name:string -> out_channel -> unit

Prints the configuration information