package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

dune-project

Dependency

sha256=667908bdd88f0bb1b75d2fa76a483006d600c9422a2a15297a172e62c0415cad

sha512=42f8e5ad308702f77c9dc40243acd2e656b16bdb94c302306dbb87387cc36941deccd5f52c18d1a045467030ddf86528b22819522a647eee5b9e1ac25f4a9560

Flèche memo / cache tables, with some advanced features

type input

type output

For now, to generalize later if needed

val eval : token:Coq.Limits.Token.t -> input -> (output, Loc.t) Coq.Protect.E.t

eval i Eval an input i

val evalS : 
  token:Coq.Limits.Token.t ->
  input ->
  (output, Loc.t) Coq.Protect.E.t * Stats.t

eval i Eval an input i and produce stats

val size : unit -> int

size () Return the cache size in words, expensive

val all_freqs : unit -> int list

freqs (): (sorted) histogram

val stats : unit -> Hashtbl.statistics

stats (): hashtbl stats

val input_info : input -> string

debug data for input

val clear : unit -> unit

clears the cache