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.7.8.16.tbz
sha256=6a88fdb3e42994204f5d2cbc8f4e7da2ac7cf28568a93c8455464c05d1087022
sha512=38c417cc28a3a0d5eb4305ee5239a0cda6ba425d7f22a17f8d3ec7b9baf27598f57fd9d5ee9a44584a3730b6105128f774abeaf2eb560cfc8bb612aa95fcc0b7

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

Module Fleche.DocSource

Sourcemodule Node : sig ... end
Sourcemodule Completion : sig ... end
Sourcetype t = private {
  1. uri : Lang.LUri.File.t;
  2. version : int;
  3. contents : Contents.t;
  4. toc : Lang.Range.t CString.Map.t;
  5. root : Coq.State.t;
  6. nodes : Node.t list;
  7. diags_dirty : bool;
  8. completed : Completion.t;
}

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

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

Return the list of all asts in the doc

Sourceval diags : t -> Lang.Diagnostic.t list

Return the list of all diags in the doc

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

Create a new Coq document, this is cached!

Sourceval bump_version : version:int -> raw:string -> t -> t Contents.R.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 : io:Io.CallBack.t -> target:Target.t -> doc:t -> unit -> t

check ~io ~target ~doc (), check document doc, target will have Flèche stop after the point specified there has been reached. Output functions are in the io record, used to send partial updates.

Sourceval save : doc:t -> (unit, Loc.t) Coq.Protect.E.t

save ~doc will save doc .vo file. It will fail if proofs are open, or if the document completion status is not Yes

Sourceval create_failed_permanent : state:Coq.State.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t Contents.R.t

This is internal, to workaround the Coq multiple-docs problem