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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.boot/Boot/Env/index.html

Module Boot.EnvSource

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:

  • http://projects.camlcity.org/projects/dl/findlib-1.9.1/doc/ref-html/lib/index.html
  • https://dune.readthedocs.io/en/stable/sites.html#sites

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:

  • the ROCQLIB env variable will be used if set
  • if not, the existence of theories/Init/Prelude.vo will be checked, in the following order:
  1. coqlibsuffix given in configure
  2. coqlib given in configure
  • if none of the above succeeds, the initialization will fail
  • The ROCQRUNTIMELIB 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.

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

Sourcetype t

Rocq runtime enviroment, including location of Rocq's Corelib

Sourcetype maybe_env =
  1. | Env of t
  2. | Boot
Sourceval initialized : unit -> maybe_env option

Returns None if the environment has not been initialized.

Sourceval init_with : coqlib:string option -> t

Init, possibly with a user provided coqlib

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

Sourceval ignored_coqlib_msg : string

Usual messsage used for warn_ignored_coqlib

Sourceval print_queries_maybe_init : warn_ignored_coqlib:(unit -> unit) -> boot:bool -> coqlib:string option -> Usage.specific_usage option -> Usage.query list -> (maybe_env, string) 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.

Sourceval corelib : t -> Path.t

Corelib directory

Sourceval plugins : t -> Path.t

plugins directory

Sourceval user_contrib : t -> Path.t

user contrib directory

Sourceval tool : t -> string -> Path.t

tool-specific directory

Sourceval native_cmi : t -> string -> Path.t

.cmi files needed for native compilation

Sourceval revision : t -> Path.t

The location of the revision file

Sourceval runtimelib : t -> Path.t

rocq-runtime/lib directory, not sure if to keep this

Sourceval coqlib : t -> Path.t

coq/lib directory, not sure if to keep this

Sourceval ocamlfind : unit -> string

camlfind () is the path to the ocamlfind binary.

Sourceval print_config : ?prefix_var_name:string -> t -> out_channel -> unit
Sourceval relocate : Coq_config.relocatable_path -> string
Sourceval rocqbin : string