Merge pull request #181 from ejgallego/perf_data

[code] [protocol] Add notification about document perf data.

CHANGES.md

@@ -15,6 +15,8 @@
    (@ejgallego, #444, reported by Alex Sanchez-Stern)
  - Display the list of pending obligations in info panel (@ejgallego,
    #262)
+ - Preliminary support to display document performance data in panel
+   (@ejgallego, #181)
 
 # coq-lsp 0.1.6: Peek
 ---------------------

controller/doc_manager.ml

@@ -158,6 +158,13 @@ let send_diags ~ofn ~doc =
   in
   ofn diags
 
+let send_perf_data ~ofn ~(doc : Fleche.Doc.t) =
+  match doc.completed with
+  | Yes _ ->
+    let params = Perf.make doc in
+    Lsp.Base.mk_notification ~method_:"$/coq/filePerfData" ~params |> ofn
+  | _ -> ()
+
 module Check : sig
   val schedule : uri:Lang.LUri.File.t -> unit
   val deschedule : uri:Lang.LUri.File.t -> unit
@@ -185,6 +192,8 @@ end = struct
       let requests = Handle.update_doc_info ~handle ~doc in
       send_diags ~ofn ~doc;
       (* Only if completed! *)
+      if completed ~doc then send_perf_data ~ofn ~doc;
+      (* Only if completed! *)
       if completed ~doc then pending := None;
       requests
     | None ->

controller/perf.ml

@@ -0,0 +1,44 @@
+(************************************************************************)
+(* Coq Language Server Protocol -- Requests                             *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+let rec list_take n = function
+  | [] -> []
+  | x :: xs -> if n = 0 then [] else x :: list_take (n - 1) xs
+
+let mk_loc_time (n : Fleche.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.Fleche.Doc.Node.range in
+  Lsp.JFleche.SentencePerfData.{ loc; time; mem }
+
+let get_stats ~(doc : Fleche.Doc.t) =
+  match List.rev doc.nodes with
+  | [] -> "no stats"
+  | n :: _ -> Fleche.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 : Fleche.Doc.t) =
+  let n_stm = List.length doc.nodes in
+  let stats = get_stats ~doc in
+  let cache_size =
+    if display_cache_size then Fleche.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 Fleche.Stats.pp_words cache_size
+  in
+  let top =
+    List.stable_sort
+      (fun (n1 : Fleche.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
+  Lsp.JFleche.DocumentPerfData.({ summary; timings } |> to_yojson)

controller/perf.mli

@@ -0,0 +1,8 @@
+(************************************************************************)
+(* Coq Language Server Protocol -- Requests                             *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+val make : Fleche.Doc.t -> Yojson.Safe.t

coq/ast.ml

@@ -62,11 +62,11 @@ let pp_loc ?(print_file = false) fmt loc =
   let file =
     if print_file then
       match loc.fname with
-      | ToplevelInput -> "Toplevel input"
-      | InFile { file; _ } -> "File \"" ^ file ^ "\""
-    else "loc"
+      | ToplevelInput -> "Toplevel input: "
+      | InFile { file; _ } -> "File \"" ^ file ^ "\": "
+    else ""
   in
-  Format.fprintf fmt "%s: line: %d, col: %d -- line: %d, col: %d / {%d-%d}" file
+  Format.fprintf fmt "%sline: %d, col: %d -- line: %d, col: %d / {%d-%d}" file
     (loc.line_nb - 1) (loc.bp - loc.bol_pos) (loc.line_nb_last - 1)
     (loc.ep - loc.bol_pos_last)
     loc.bp loc.ep

editor/code/esbuild.mjs

@@ -78,5 +78,6 @@ function viewBuild(file) {
 }
 
 var infoView = viewBuild("./views/info/index.tsx");
+var perfView = viewBuild("./views/perf/index.tsx");
 
-await Promise.all[(node, browser, infoView)];
+await Promise.all[(node, browser, infoView, perfView)];

editor/code/lib/types.ts

@@ -108,3 +108,14 @@ export interface FlecheDocument {
 export interface FlecheSaveParams {
   textDocument: VersionedTextDocumentIdentifier;
 }
+
+export interface SentencePerfParams {
+  loc: Loc;
+  time: number;
+  mem: number;
+}
+
+export interface DocumentPerfParams {
+  summary: string;
+  timings: SentencePerfParams[];
+}