package vsrocq-language-server

  1. Overview
  2. Docs
VSRocq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (8)

Authors

  1. E
    Enrico Tassi
  2. M
    Maxime Dénès
  3. R
    Romain Tetley

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

vsrocq-language-server-2.5.0.tar.gz
md5=15c22fee2131c4b3dae4258e8a4484f6
sha512=b5ab3eea5bb6af643d635781e741a7a7b217fcc33e84c2c9e3448962118a63e174569ef6069c50af2ab57508d5cef476a8cfade14957a9654b1fea16c29a08b9

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

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

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
Sourcetype execution_result_ = {
  1. updates : (Types.sentence_id * Types.sentence_checking_result) list;
  2. vs : Vernacstate.t;
  3. events : events;
  4. exec_error : errored_sentence;
}
Sourcetype internal
Sourceval interrupt_execution : state -> unit
Sourcemodule ProofWorkerProcess : sig ... end

Rocq toplevels for delegation without fork