package vscoq-language-server

You can search for identifiers within the package.

in-package search v0.2.0

VSCoq language server

Install

Dune Dependency

github.com Readme Edit opam file Versions (14)

Authors

Maintainers

E

Enrico Tassi <enrico.tassi@inria.fr>

Sources

vscoq-language-server-2.2.5.tar.gz

md5=8bc848aaf2ad0fe41a02741e633ad7e3

sha512=eb6c80a3290b1d688ea3b94a3087f204c9f9f03bddd95b21952b02af1dc4de073c1b99baed5a5f6a395e69a27c0d45f6ec181488da62e9f5c6a77d91d752dd5c

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

Module `Dm.Scheduler`Source

The scheduler is the component in charge of planning the execution of sentences. It also defines the task delegation strategy, and computes dependencies between tasks. Scheduling can be done incrementally.

Sourcetype state

State for incremental schedule construction

Sourceval initial_state : state

Sourcetype error_recovery_strategy =

| RSkip
| RAdmitted

Sourcetype executable_sentence = {

id : Types.sentence_id;
ast : Synterp.vernac_control_entry;
classif : Vernacextend.vernac_classification;
synterp : Vernacstate.Synterp.t;
error_recovery : error_recovery_strategy;

}

Sourcetype task =

| Skip of {
1. id : Types.sentence_id;
2. error : Pp.t option;
}
| Block of {
1. id : Types.sentence_id;
2. error : Pp.t Loc.located;
}
| Exec of executable_sentence
| OpaqueProof of {
1. terminator : executable_sentence;
2. opener_id : Types.sentence_id;
3. proof_using : Vernacexpr.section_subset_expr;
4. tasks : executable_sentence list;
}
| Query of executable_sentence

Sourcetype schedule

Holds the dependencies among sentences and a schedule to evaluate all sentences

Sourceval initial_schedule : schedule

Source

val schedule_errored_sentence : 
  Types.sentence_id ->
  Pp.t Loc.located ->
  schedule ->
  schedule

Source

val schedule_sentence : 
  (Types.sentence_id
   * (Synterp.vernac_control_entry
      * Vernacextend.vernac_classification
      * Vernacstate.Synterp.t)) ->
  state ->
  schedule ->
  state * schedule

Identifies the structure of the document and dependencies between sentences in order to easily compute the tasks to interpret the a sentence. Input sentence is None on parsing error.

Source

val task_for_sentence : 
  schedule ->
  Types.sentence_id ->
  Types.sentence_id option * task

Finds the task to be performed and the state on which the task should run

Sourceval dependents : schedule -> Types.sentence_id -> Types.sentence_id_set

Computes what should be invalidated

Sourceval string_of_schedule : schedule -> string

package vscoq-language-server

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Dm.SchedulerSource

Module `Dm.Scheduler`Source