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=764f5cbaf3da308a21ea2953a275e74b6e5a841c82bdd8b71fa474b1395738a1

sha512=16189385a27ce7576820d03d4410d4f9bc52150b43d714813c3611d6b5519b5d256c1ac348913bbf77c6f313d54927ead935a188783e04b21032f5e06c793778

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, Coq.Loc_t.t) Coq.Protect.E.t

eval i Eval an input i

val evalS : 
  token:Coq.Limits.Token.t ->
  input ->
  (output, Coq.Loc_t.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