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 (5)

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.vernac/Mltop/index.html

Module MltopSource

Toplevel management
Sourcemodule PluginSpec : sig ... end

Coq plugins are identified by their OCaml library name (in the Findlib sense)

Sourcetype toplevel = {
  1. load_plugin : PluginSpec.t -> unit;
    (*

    Load a findlib library, given by public name

    *)
  2. load_module : string -> unit;
    (*

    Load a cmxs / cmo module, used by the native compiler to load objects

    *)
  3. add_dir : string -> unit;
    (*

    Adds a dir to the module search path

    *)
  4. ml_loop : ?init_file:string -> unit -> unit;
    (*

    Run the OCaml toplevel with given addtitional initialisation file

    *)
}
Sourceval set_top : toplevel -> unit

Sets and initializes a toplevel (if any)

Sourceval load_module : string -> unit

Low level module loading, for the native compiler and similar users.

Sourceval remove : unit -> unit

Removes the toplevel (if any)

Sourceval is_ocaml_top : unit -> bool

Tests if an Ocaml toplevel runs under Coq

Sourceval ocaml_toploop : ?init_file:string -> unit -> unit

Starts the Ocaml toplevel loop

Sourceval add_ml_dir : string -> unit

Adds a dir to the plugin search path, this also extends OCamlfind's search path

Tests if we can load ML files

Initialization functions
Sourceval add_init_function : string -> (unit -> unit) -> unit

Declare a initialization function. The initialization function is called in Declare ML Module, including reruns after backtracking over it (either interactive backtrack, module closing backtrack, Require of a file with Declare ML Module).

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

Register a callback that will be called when the module is declared with the Declare ML Module command. This is useful to define Coq objects at that time only. Several functions can be defined for one module; they will be called in the order of declaration, and after the ML module has been properly initialized.

Unlike the init functions it does not run after closing a module or Requiring a file which contains the Declare ML Module. This allows to have effects which depend on the module when command was run in, eg add a named libobject which will use it for the prefix.

The callback runs in the synterp phase, use declare_cache_obj_full if you also need to interact with Interp state.

Sourcetype cache_obj =
  1. | CacheObj : {
    1. synterp : unit -> 'a;
    2. interp : 'a -> unit;
    } -> cache_obj
Sourceval interp_only_obj : (unit -> unit) -> cache_obj
Sourceval declare_cache_obj_full : cache_obj -> string -> unit

Register a callback with an interp phase.

Declaring modules
Sourcetype interp_fun
Sourceval run_interp_fun : interp_fun -> unit
Sourceval declare_ml_modules : Vernacexpr.locality_flag -> string list -> interp_fun

Implementation of the Declare ML Module vernacular command.

Utilities
Sourceval print_ml_modules : unit -> Pp.t
Sourceval print_gc : unit -> Pp.t