package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

coq-lsp-0.1.7.8.16.tbz
sha256=6a88fdb3e42994204f5d2cbc8f4e7da2ac7cf28568a93c8455464c05d1087022
sha512=38c417cc28a3a0d5eb4305ee5239a0cda6ba425d7f22a17f8d3ec7b9baf27598f57fd9d5ee9a44584a3730b6105128f774abeaf2eb560cfc8bb612aa95fcc0b7

doc/src/coq-lsp.fleche/perf_analysis.ml.html

Source file perf_analysis.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
open Perf

let rec list_take n = function
  | [] -> []
  | x :: xs -> if n = 0 then [] else x :: list_take (n - 1) xs

let mk_loc_time (n : Doc.Node.t) =
  let time = Option.default 0.0 n.info.time in
  let mem = n.info.mw_after -. n.info.mw_prev in
  let loc = n.Doc.Node.range in
  Sentence.{ loc; time; mem }

let get_stats ~(doc : Doc.t) =
  match List.rev doc.nodes with
  | [] -> "no stats"
  | n :: _ -> Stats.to_string n.info.stats

(** Turn into a config option at some point? This is very expensive *)
let display_cache_size = false

let make (doc : Doc.t) =
  let n_stm = List.length doc.nodes in
  let stats = get_stats ~doc in
  let cache_size =
    if display_cache_size then Memo.Interp.size () |> float_of_int else 0.0
  in
  let summary =
    Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@\n}" n_stm
      stats Stats.pp_words cache_size
  in
  let top =
    List.stable_sort
      (fun (n1 : Doc.Node.t) n2 -> compare n2.info.time n1.info.time)
      doc.nodes
  in
  let top = list_take 10 top in
  let timings = List.map mk_loc_time top in
  { summary; timings }
OCaml

Innovation. Community. Security.