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.0.8.17.tbz
sha256=36340f464107ac60bb4033fad249984690cdcce3a6bef4ca439ffb2a4458dbf9
sha512=4866f4c2f0acda0c114e27b32cd60fa054333e1c7249227b8c3b23a316d7f306676203bd317f135a40368a292b7b49b76f0bdacff21d7e9bfb5a422d1c8d6ad8

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

Module Fleche.DocSource

Sourcemodule Node : sig ... end
Sourcemodule Completion : sig ... end
Sourcemodule Env : sig ... end

Enviroment external to the document, this includes for now the init Coq state and the workspace, which are used to build the first state of the document, usually by importing the prelude and other libs implicitly.

Sourcetype t = private {
  1. uri : Lang.LUri.File.t;
    (*

    uri of the document

    *)
  2. version : int;
    (*

    version of the document

    *)
  3. contents : Contents.t;
    (*

    contents of the document

    *)
  4. nodes : Node.t list;
    (*

    List of document nodes

    *)
  5. completed : Completion.t;
    (*

    Status of the document, usually either completed, suspended, or waiting for some IO / external event

    *)
  6. toc : Node.t CString.Map.t;
    (*

    table of contents

    *)
  7. env : Env.t;
    (*

    External document enviroment

    *)
  8. root : Coq.State.t;
    (*

    root contains the first state document state, obtained by applying a workspace to Coq's initial state

    *)
  9. diags_dirty : bool;
    (*

    internal field

    *)
}

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 : token:Coq.Limits.Token.t -> env:Env.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t

Create a new Coq document, this is cached! Note that this operation always suceeds, but the document could be created in a `Failed` state if problems arise.

Sourceval bump_version : token:Coq.Limits.Token.t -> version:int -> raw:string -> t -> t

Update the contents of a document, updating the right structures for incremental checking. If the operation fails, the document will be left in `Failed` state.

Sourcemodule Target : sig ... end

Checking targets, this specifies what we expect check to reach

Sourceval check : io:Io.CallBack.t -> token:Coq.Limits.Token.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 : token:Coq.Limits.Token.t -> 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