(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** 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:
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: + [coqlibsuffix] given in configure + [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.
*)
module Path : sig
(** This API is loosely inspired by [Stdune.Path], for now we keep
it minimal, but at some point we may extend it. *)
(** Paths are private, and owned by the functions below *) type t
(** [relative path string] build a path relative to an existing one *) val relative : t -> string -> t
(** We should gradually add some more functions to handle common dirs here such the theories directories or share files. Abstracting it
hereere does allow to use system-specific functionalities *)
(** [exists file] checks if [file] exists *) valexists : t -> bool
(** String representation *) val to_string : t -> string
end
(** Rocq runtime enviroment, including location of Rocq's Corelib *) type t
type maybe_env =
| Env of t
| Boot
(** Returns [None] if the environment has not been initialized. *) val initialized : unit -> maybe_env option
(** Init, possibly with a user provided coqlib *) val init_with : coqlib:stringoption -> t
(** Init if boot:false, possibly with a user provided coqlib.
Incompatible arguments run [warn_ignored_coqlib] (ie with boot:true and coqlib:Some) *) val maybe_init : warn_ignored_coqlib:(unit -> unit) ->
boot:bool -> coqlib:stringoption -> maybe_env
(** Usual messsage used for warn_ignored_coqlib *) val ignored_coqlib_msg : string
(** 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].
*) val print_queries_maybe_init : warn_ignored_coqlib:(unit -> unit) ->
boot:bool -> coqlib:stringoption ->
Usage.specific_usage option -> Usage.query list -> (maybe_env, string) result
(** [Corelib directory] *) val corelib : t -> Path.t
(** [plugins directory] *) val plugins : t -> Path.t
(** [user contrib directory] *) val user_contrib : t -> Path.t
(** [tool-specific directory] *) val tool : t -> string -> Path.t
(** .cmi files needed for native compilation *) val native_cmi : t -> string -> Path.t
(** The location of the revision file *) val revision : t -> Path.t
(** rocq-runtime/lib directory, not sure if to keep this *) val runtimelib : t -> Path.t
(** coq/lib directory, not sure if to keep this *) val coqlib : t -> Path.t
(** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string
val print_config : ?prefix_var_name:string -> t -> out_channel -> unit
val relocate : Coq_config.relocatable_path -> string
val rocqbin : string
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
