package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (35)

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.1.4.v8.16.tbz
sha256=50df59eafc5b24a881c1a1dda6f6032b1da35b9b6ade7cb9e39968def9319508
sha512=e1d383b6802758cdbe5cbc6278af275d7951acd78224cdcfe622428942e84366ca283bf375d6e535ad7e8d8e847df84bd763bb2a263fc457dc5aead386c2836d

doc/coq-lsp.fleche/Fleche/Doc/index.html

Module Fleche.DocSource

Sourcemodule Node : sig ... end
Sourcemodule Contents : sig ... end
Sourcemodule Completion : sig ... end
Sourcetype t = private {
  1. uri : string;
  2. version : int;
  3. contents : Contents.t;
  4. root : Coq.State.t;
  5. nodes : Node.t list;
  6. diags_dirty : bool;
  7. completed : Completion.t;
}

A Flèche document is basically a node list, which is a crude form of a meta-data map Loc.t -> data, where for now data is the contents of Node.t.

Sourceval asts : t -> Coq.Ast.t list

Return the list of all asts in the doc

Sourceval create : state:Coq.State.t -> workspace:Coq.Workspace.t -> uri:string -> version:int -> contents:string -> (t, Loc.t) Coq.Protect.R.t

Note, create calls Coq but it is not cached in the Memo.t table

Sourceval bump_version : version:int -> contents:string -> t -> t

Update the contents of a document, updating the right structures for incremental checking.

Sourcemodule Target : sig ... end

Checking targets, this specifies what we expect check to reach

Sourceval check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t

check ~ofmt ~target ~doc (), target will have Flèche stop after the point specified there has been reached.