package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Node : sig ... end
module Completion : sig ... end
module 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.

type 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.

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

Return the list of all asts in the doc

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

Return the list of all diags in the doc

val 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.

val 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.

module Target : sig ... end

Checking targets, this specifies what we expect check to reach

val 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.

val 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

val run : token:Coq.Limits.Token.t -> ?loc:Loc.t -> ?memo:bool -> st:Coq.State.t -> string -> (Coq.State.t, Loc.t) Coq.Protect.E.t

run ~token ?loc ?memo ~st cmds run commands cmds starting on state st, without commiting changes to the document. loc can be used to seed an initial location if desired, if not the locations will be considered relative to the initial location. memo controls if the execution is memoized, by default true.

This API is experimental, used for speculative execution petanque and goals, the API is expected to change as to better adapt to users.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct