package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223
doc/src/coq-lsp.fleche/stats.ml.html
Source file stats.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 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
(************************************************************************) (* Coq Language Server Protocol *) (* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) (* Copyright 2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) (* Status: Experimental *) (************************************************************************) module Kind = struct type t = | Hashing | Parsing | Exec end type t = { time : float ; memory : float } let stats : (Kind.t, t) Hashtbl.t = Hashtbl.create 1000 let z = { time = 0.0; memory = 0.0 } let find kind = Hashtbl.find_opt stats kind |> Option.default z module Global = struct type nonrec 'a stats = t type nonrec t = t * t * t let zero () = (z, z, z) let dump () = (find Kind.Hashing, find Kind.Parsing, find Kind.Exec) let restore (h, p, e) = Hashtbl.replace stats Kind.Hashing h; Hashtbl.replace stats Kind.Parsing p; Hashtbl.replace stats Kind.Exec e let get_f (h, p, e) ~kind = match kind with | Kind.Hashing -> h | Parsing -> p | Exec -> e let to_string (h, p, e) = Format.asprintf "hashing: %f | parsing: %f | exec: %f" h.time p.time e.time end let bump kind { time; memory } = let acc = find kind in let time = acc.time +. time in let memory = acc.memory +. memory in Hashtbl.replace stats kind { time; memory } let time_and_mem f x = let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in let before = Unix.gettimeofday () in let v = f x in let after = Unix.gettimeofday () in let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in let time = after -. before in let memory = mw_after -. mw_prev in (v, { time; memory }) let record ~kind ~f x = let res, stats = time_and_mem f x in bump kind stats; (res, stats) let get_accumulated ~kind = find kind let reset () = Hashtbl.remove stats Kind.Hashing; Hashtbl.remove stats Kind.Parsing; Hashtbl.remove stats Kind.Exec; () let mb = 1024 * 1024 let pp_words fmt w = (* Format is not working great for floating point values... *) let w = int_of_float w in let value, spec = if w < 1024 then (w, "w ") else if w < mb then (w / 1024, "Kw") else (w / mb, "Mw") in Format.fprintf fmt "@[%4d %s@]" value spec
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>