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.2.4.9.1.tbz
sha256=667908bdd88f0bb1b75d2fa76a483006d600c9422a2a15297a172e62c0415cad
sha512=42f8e5ad308702f77c9dc40243acd2e656b16bdb94c302306dbb87387cc36941deccd5f52c18d1a045467030ddf86528b22819522a647eee5b9e1ac25f4a9560

doc/coq-lsp.coq/Coq/Library_file/index.html

Module Coq.Library_fileSource

Sourcetype t
Sourceval name : t -> Names.DirPath.t

Logical path of the library

Sourcemodule Entry : sig ... end
Sourceval toc : token:Limits.Token.t -> st:State.t -> t list -> (Entry.t list, Loc.t) Protect.E.t

toc libs Returns the list of constants and inductives found on .vo libraries libs, as pairs of name, typ. Note that the constants are returned in the order they appear on the file.

NOTE that (unfortunately) this is a very expensive process, similary to Coq's Search, as this routine will have to traverse all the library objects in scope.

Hence, we provide a slightly more efficient version that can do multiple libraries but with the same complexity.

There have been several upstream Coq PRs trying to improve this situation, but so far they didn't make enough progress.

Sourceval loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t

Recovers the list of loaded libraries for state st