package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.2.8.19.tbz
sha256=1a0639b7774a79c8489b3e7e1ea606a24c857dc70833bbafb79b6d620c18b2b1
sha512=32782243b628fc8a92100778816772baf304335f35518e330c6c4a1b22b2139e255610f2091b47def590877455d361e22beab8ecc4f06b3f13da4e75a576fa07
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)"
>