package vscoq-language-server

  1. Overview
  2. Docs
VSCoq language server

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (15)

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

vscoq-language-server-2.1.0-coq8.19.tar.gz
md5=7bdc4ae44d8d6ab21d586e20835a1b79
sha512=7ab8ddae303a9b9ec2d62338edbf4176ca1146ed29e34eb02cf41fc91bf21d507c6e571ba30b73e45869d25a750d7915e79b915d962629cb9aed1598e0b68795

doc/vscoq-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 feedback_message = Feedback.level * Loc.t option * 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)) list
Sourceval all_feedback : state -> (Types.sentence_id * feedback_message) list
Sourceval shift_diagnostics_locs : state -> start:int -> offset:int -> state
Sourceval executed_ids : state -> Types.sentence_id list
Sourceval is_executed : state -> Types.sentence_id -> bool
Sourceval is_remotely_executed : state -> Types.sentence_id -> bool
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 -> 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 execute : state -> (Vernacstate.t * events * bool) -> prepared_task -> state * Vernacstate.t * events * bool
Sourcemodule ProofWorkerProcess : sig ... end

Coq toplevels for delegation without fork