Module `Stm`Source

state-transaction-machine interface

Sourcemodule AsyncOpts : sig ... end

Sourcetype stm_doc_type =

| VoDoc of string
| VioDoc of string
| 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 = {

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.
*)
injections : Coqargs.injection_command list;
(*
Injects Require and Set/Unset commands before the initial state is ready
*)
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

Sourceval new_doc : stm_init_options -> doc * Stateid.t

new_doc opt Creates a new document with options opt

Source

val 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 =

| NewAddTip
| Unfocus of Stateid.t

Source

val 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

Source

val query : 
  doc:doc ->
  at:Stateid.t ->
  route:Feedback.route_id ->
  Pcoq.Parsable.t ->
  unit

Sourcetype focus = {

start : Stateid.t;
stop : Stateid.t;
tip : Stateid.t;

}

Sourcetype edit_focus =

| NewTip
| 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

Source

val snapshot_vio : 
  create_vos:bool ->
  doc:doc ->
  output_native_objects:bool ->
  Names.DirPath.t ->
  string ->
  doc

Sourceval reset_task_queue : unit -> unit

Sourcetype document

Sourcetype tasks = (Opaqueproof.opaque_handle option, document) Library.tasks

Sourceval check_task : string -> tasks -> int -> bool

Sourceval info_tasks : tasks -> (string * float * int) list

Source

val finish_tasks : 
  string ->
  Library.seg_univ ->
  Library.seg_proofs ->
  tasks ->
  Library.seg_univ * Library.seg_proofs

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 **************************************************************** *

Sourcemodule ProofTask : AsyncTaskQueue.Task

Sourcemodule QueryTask : AsyncTaskQueue.Task

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

Sourcemodule DynBlockData : Dyn.S

Sourcetype static_block_declaration = {

block_start : Stateid.t;
block_stop : Stateid.t;
dynamic_switch : Stateid.t;
carry_on_data : DynBlockData.t;

}

Sourcetype document_node = {

indentation : int;
ast : Vernacexpr.vernac_control;
id : Stateid.t;

}

Sourcetype document_view = {

entry_point : document_node;
prev_node : document_node -> document_node option;

}

Sourcetype static_block_detection = document_view -> static_block_declaration option

Sourcetype recovery_action = {

base_state : Stateid.t;
goals_to_admit : Goal.goal list;
recovery_command : Vernacexpr.vernac_control option;

}

Sourcetype block_classification =

| ValidBlock of recovery_action
| Leaks

Source

type dynamic_block_error_recovery =
  doc ->
  static_block_declaration ->
  block_classification

Source

val register_proof_block_delimiter : 
  Vernacextend.proof_block_name ->
  static_block_detection ->
  dynamic_block_error_recovery ->
  unit

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

Source

val state_computed_hook : 
  (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t

Source

val 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 =

| Valid of Vernacstate.t option
| Expired
| 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.stm/Stm/index.html

Module `Stm`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.stm/Stm/index.html

Module StmSource

Module `Stm`Source