package vscoq-language-server

  1. Overview
  2. Docs
package vscoq-language-server
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Dm.ExecutionManagerSource

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 =
  1. | CheckProofsInMaster
  2. | SkipProofs
  3. | DelegateProofsToWorkers of {
    1. number_of_workers : int;
    }
Sourcetype options = {
  1. delegation_mode : delegation_mode;
  2. completion_options : Protocol.Settings.Completion.t;
  3. 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 destroy : state -> unit
Sourceval get_options : unit -> options
Sourceval set_options : options -> unit
Sourceval set_default_options : unit -> unit
Sourceval error : state -> Types.sentence_id -> (Loc.t option * Pp.t) option
Sourceval 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
Sourceval 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

Sourceval 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

Sourceval 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
Sourceval update_processed : Types.sentence_id -> state -> Document.document -> state
Sourceval prepare_overview : state -> Protocol.LspWrapper.Range.t list -> state
Sourceval print_exec_overview_of_state : state -> unit
Sourcemodule ProofWorkerProcess : sig ... end

Coq toplevels for delegation without fork

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