package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module StmSource

state-transaction-machine interface

Sourcemodule AsyncOpts : sig ... end
Sourcetype stm_doc_type =
  1. | VoDoc of string
  2. | VioDoc 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

    *)
  3. stm_options : AsyncOpts.stm_opt;
    (*

    Low-level STM options

    *)
}

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 snapshorts 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 Pcoq.Entry.t) -> Pcoq.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 -> Pcoq.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 -> doc
Sourceval finish : doc:doc -> doc
Sourceval wait : doc:doc -> doc
Sourceval stop_worker : string -> unit
Sourceval join : doc:doc -> doc
Sourceval snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> Names.DirPath.t -> string -> doc
Sourceval reset_task_queue : unit -> unit
Sourcetype document
Sourceval check_task : string -> tasks -> int -> bool
Sourceval info_tasks : tasks -> (string * float * int) list
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
Sourceval set_perspective : doc:doc -> Stateid.t list -> 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) Hook.t
Sourceval unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t
Sourceval state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t
Sourceval forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
Sourceval document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t

User adds a sentence to the document (after parsing)

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

User edits a sentence in the document

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct