ExecutionManager (p.vsrocq-language-server.2.5.0.doc.vsrocq-language-server.dm.Dm.ExecutionManager)

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

Sourceval pr_event : event -> Pp.t

Sourceval init : Vernacstate.t -> feedback_pipe:Types.feedback_pipe -> state

Sourceval destroy : state -> unit

Sourceval get_options : unit -> options

Sourceval set_options : options -> unit

Sourceval set_default_options : unit -> unit

Sourceval invalidate : state -> Types.sentence_id -> state

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

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

Sourceval get_initial_vernac_state : state -> Vernacstate.t

Source

val handle_event : 
  Document.document ->
  event ->
  state ->
  Types.sentence_id option
  * (Types.sentence_id * Types.sentence_checking_result) 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 ->
  Vernacstate.t * prepared_task list * state * errored_sentence

Sourcetype execution_result_ = {

updates : (Types.sentence_id * Types.sentence_checking_result) list;
vs : Vernacstate.t;
events : events;
exec_error : errored_sentence;

}

Sourcetype internal

Sourcetype execution_result =

| Done of execution_result_
| WillDo of internal Sel.Promise.t * internal Sel.Promise.state -> execution_result_

Source

val execute : 
  state ->
  Document.document ->
  Vernacstate.t ->
  prepared_task ->
  state * execution_result

Source

val view_task : 
  prepared_task ->
  [ `Local of Types.sentence_id
  | `Remote of
    Types.sentence_id
    * Types.sentence_id
    * Types.sentence_id
    * Types.sentence_id ]

Sourceval interrupt_execution : state -> unit

Sourcemodule ProofWorkerProcess : sig ... end

Rocq toplevels for delegation without fork