Module `Dm.ExecutionManager`Source

The event manager is in charge of the actual event of tasks (as defined by the scheduler), caching event states and invalidating them. It can delegate to worker processes via DelegationManager

Sourcetype delegation_mode =

| CheckProofsInMaster
| SkipProofs
| DelegateProofsToWorkers of {
1. number_of_workers : int;
}

Sourcetype options = {

delegation_mode : delegation_mode;
completion_options : Protocol.Settings.Completion.t;
enableDiagnostics : bool;

}

Sourceval is_diagnostics_enabled : unit -> bool

Sourcetype state

Execution state, includes the cache

Sourcetype event

Sourcetype events = event Sel.Event.t list

Sourcetype errored_sentence = (Types.sentence_id * Loc.t option) option

Sourcetype feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t

Sourceval pr_event : event -> Pp.t

Sourceval init : Vernacstate.t -> state * event Sel.Event.t

Sourceval destroy : state -> unit

Sourceval get_options : unit -> options

Sourceval set_options : options -> unit

Sourceval set_default_options : unit -> unit

Source

val invalidate : 
  Document.document ->
  Scheduler.schedule ->
  Types.sentence_id ->
  state ->
  state

Sourceval error : state -> Types.sentence_id -> (Loc.t option * Pp.t) option

Sourceval feedback : state -> Types.sentence_id -> feedback_message list

Source

val all_errors : 
  state ->
  (Types.sentence_id * (Loc.t option * Pp.t * Quickfix.t list option)) list

Sourceval all_feedback : state -> (Types.sentence_id * feedback_message) list

Sourceval reset_overview : state -> Document.document -> state

Source

val shift_overview : 
  state ->
  before:RawDocument.t ->
  after:RawDocument.t ->
  start:int ->
  offset:int ->
  state

Sourceval shift_diagnostics_locs : state -> start:int -> offset:int -> state

Sourceval executed_ids : state -> Types.sentence_id list

Sourceval is_locally_executed : state -> Types.sentence_id -> bool

we know if it worked and we have the state in this process

Sourceval is_remotely_executed : state -> Types.sentence_id -> bool

we know if it worked but we do not have the state in this process

Source

val get_context : 
  state ->
  Types.sentence_id ->
  (Evd.evar_map * Environ.env) option

Sourceval get_initial_context : state -> Evd.evar_map * Environ.env

Sourceval get_vernac_state : state -> Types.sentence_id -> Vernacstate.t option

Returns the vernac state after the sentence

Source

val handle_event : 
  event ->
  state ->
  Types.sentence_id option * state option * events

Events for the main loop

Sourcetype prepared_task

Execution happens in two steps. In particular the event one takes only one task at a time to ease checking for interruption

Sourceval get_id_of_executed_task : prepared_task -> Types.sentence_id

Source

val build_tasks_for : 
  Document.document ->
  Scheduler.schedule ->
  state ->
  Types.sentence_id ->
  bool ->
  Vernacstate.t * state * prepared_task option * errored_sentence

Source

val execute : 
  state ->
  Document.document ->
  (Vernacstate.t * events * bool) ->
  prepared_task ->
  bool ->
  prepared_task option * state * Vernacstate.t * events * errored_sentence

Sourceval update_processed : Types.sentence_id -> state -> Document.document -> state

Sourceval prepare_overview : state -> Protocol.LspWrapper.Range.t list -> state

Sourceval overview : state -> Types.exec_overview

Source

val overview_until_range : 
  state ->
  Protocol.LspWrapper.Range.t ->
  Types.exec_overview

Sourceval print_exec_overview_of_state : state -> unit

Sourcemodule ProofWorkerProcess : sig ... end

Coq toplevels for delegation without fork

Install

Dune Dependency

Authors

Maintainers

Sources

doc/vscoq-language-server.dm/Dm/ExecutionManager/index.html

Module `Dm.ExecutionManager`Source

package vscoq-language-server

Install

Dune Dependency

Authors

Maintainers

Sources

doc/vscoq-language-server.dm/Dm/ExecutionManager/index.html

Module Dm.ExecutionManagerSource

Module `Dm.ExecutionManager`Source