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.stm/Stm/index.html

Module StmSource

state-transaction-machine interface

Sourcemodule AsyncOpts : sig ... end
Sourcetype stm_doc_type =
  1. | VoDoc of string
  2. | VosDoc of string
  3. | Interactive of Coqargs.top

The STM document type stm_doc_type determines some properties such as what uncompleted proofs are allowed and what gets recorded to aux files.

Sourcetype stm_init_options = {
  1. doc_type : stm_doc_type;
    (*

    The STM does set some internal flags differently depending on the specified doc_type. This distinction should disappear at some some point.

    *)
  2. injections : Coqargs.injection_command list;
    (*

    Injects Require and Set/Unset commands before the initial state is ready

    *)
}

STM initialization options:

Sourcetype doc

The type of a STM document

Sourceval init_process : AsyncOpts.stm_opt -> unit

init_process performs some low-level initialization, call early

Sourceval init_core : unit -> unit

init_core snapshots the initial system state

new_doc opt Creates a new document with options opt

Sourceval parse_sentence : doc:doc -> Stateid.t -> entry:(Pvernac.proof_mode option -> 'a Procq.Entry.t) -> Procq.Parsable.t -> 'a

parse_sentence sid entry pa Reads a sentence from pa with parsing state sid and non terminal entry. entry receives in input the current proof mode. sid should be associated with a valid parsing state (which may not be the case if an error was raised at parsing time).

Sourcetype add_focus =
  1. | NewAddTip
  2. | Unfocus of Stateid.t
Sourceval add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control -> doc * Stateid.t * add_focus
Sourceval get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
Sourceval get_proof : doc:doc -> Stateid.t -> Proof.t option
Sourceval query : doc:doc -> at:Stateid.t -> route:Feedback.route_id -> Procq.Parsable.t -> unit
Sourcetype focus = {
  1. start : Stateid.t;
  2. stop : Stateid.t;
  3. tip : Stateid.t;
}
Sourcetype edit_focus =
  1. | NewTip
  2. | Focus of focus
Sourceval edit_at : doc:doc -> Stateid.t -> doc * edit_focus
Sourceval observe : doc:doc -> Stateid.t -> unit
Sourceval finish : doc:doc -> Vernacstate.t
Sourceval wait : doc:doc -> unit
Sourceval stop_worker : string -> unit
Sourceval join : doc:doc -> unit
Sourceval snapshot_vos : doc:doc -> output_native_objects:bool -> Names.DirPath.t -> string -> unit
Sourceval reset_task_queue : unit -> unit
Sourcetype document
Sourceval get_current_state : doc:doc -> Stateid.t
Sourceval get_ldir : doc:doc -> Names.DirPath.t
Sourceval get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option
Sourceval set_compilation_hints : string -> unit

workers **************************************************************** *

document structure customization *************************************** *

Sourcetype static_block_declaration = {
  1. block_start : Stateid.t;
  2. block_stop : Stateid.t;
  3. dynamic_switch : Stateid.t;
  4. carry_on_data : DynBlockData.t;
}
Sourcetype document_node = {
  1. indentation : int;
  2. ast : Vernacexpr.vernac_control;
  3. id : Stateid.t;
}
Sourcetype document_view = {
  1. entry_point : document_node;
  2. prev_node : document_node -> document_node option;
}
Sourcetype static_block_detection = document_view -> static_block_declaration option
Sourcetype recovery_action = {
  1. base_state : Stateid.t;
  2. goals_to_admit : Evar.t list;
  3. recovery_command : Vernacexpr.vernac_control option;
}
Sourcetype block_classification =
  1. | ValidBlock of recovery_action
  2. | Leaks
Sourcetype dynamic_block_error_recovery = doc -> static_block_declaration -> block_classification

customization ********************************************************** *

Sourceval state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) -> unit
Sourceval unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) -> unit
Sourceval state_ready_hook : (doc:doc -> Stateid.t -> unit) -> unit
Sourceval forward_feedback_hook : (Feedback.feedback -> unit) -> unit
Sourceval document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) -> unit

User adds a sentence to the document (after parsing)

Sourceval document_edit_hook : (Stateid.t -> unit) -> unit

User edits a sentence in the document

Sourceval sentence_exec_hook : (Stateid.t -> unit) -> unit

User requests evaluation of a sentence

Sourceval get_doc : Feedback.doc_id -> doc
Sourcetype state =
  1. | Valid of Vernacstate.t option
  2. | Expired
  3. | Error of exn
Sourceval state_of_id : doc:doc -> Stateid.t -> state
Sourceval current_proof_depth : doc:doc -> int
Sourceval get_all_proof_names : doc:doc -> Names.Id.t list
Sourceval stm_debug : bool ref

Enable STM debugging

Sourceval backup : unit -> document
Sourceval restore : document -> unit