[perf] Fixes and improvements towards more interesting uses.

Motivated by the nice heatmap (PR #686) , we fix and improve perf data, in particular, we - we now send data for all the sentences, not only for the top 10 - we send data that takes into account the cached execution of the command - we include a client-side option to disable sending of this data, as it can be "large" for large files (not so much actually, but just in case) - we fix types.ts for Loc -> Range (seems to be a bug from the beginning) Co-authored-by: Ali Caglayan <alizter@gmail.com>
ejgallego · May 2, 2024 · 25cb3e1 · 25cb3e1
1 parent 56ea2a2
commit 25cb3e1
Show file tree

Hide file tree

Showing 12 changed files with 185 additions and 62 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -98,6 +98,7 @@
  - Update `package-lock.json` for latest bugfixes (@ejgallego, #687)
  - Update Nix flake enviroment (@Alizter, #684 #688)
  - Update `prettier` (@Alizter @ejgallego, #684 #688)
+ - Fixes to perf (TODO) (@ejgallego @Alizter, #699)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts
@@ -31,6 +31,7 @@ export interface Message<Pp> {
 
 export type Id = ["Id", string];
 
+// XXX: Only used in obligations, move them to Range
 export interface Loc {
   fname: any;
   line_nb: number;
@@ -113,12 +114,22 @@ export interface FlecheSaveParams {
   textDocument: VersionedTextDocumentIdentifier;
 }
 
-export interface SentencePerfParams {
-  loc: Loc;
+export interface PerfInfo {
+  // Original Execution Time (when not cached)
   time: number;
+  // Whether the execution was cached
+  cached: boolean;
+  // "Real" Execution Time, often very low for memoized sentences
+  real: number;
+  // Difference in words allocated in the heap using `Gc.quick_stat`
   mem: number;
 }
 
+export interface SentencePerfParams {
+  range: Range;
+  info: PerfInfo;
+}
+
 export interface DocumentPerfParams {
   textDocument: VersionedTextDocumentIdentifier;
   summary: string;
@@ -152,3 +163,19 @@ export type CoqMessagePayload = RenderGoals | WaitingForInfo | InfoError;
 export interface CoqMessageEvent extends MessageEvent {
   data: CoqMessagePayload;
 }
+
+// For perf panel data
+export interface PerfUpdate {
+  method: "update";
+  params: DocumentPerfParams;
+}
+
+export interface PerfReset {
+  method: "reset";
+}
+
+export type PerfMessagePayload = PerfUpdate | PerfReset;
+
+export interface PerfMessageEvent extends MessageEvent {
+  data: PerfMessagePayload;
+}
diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
@@ -210,9 +210,14 @@ export function activateCoqLSP(
 
   const goals = (editor: TextEditor) => {
     if (!client.isRunning()) return;
-    let uri = editor.document.uri;
+    let uri = editor.document.uri.toString();
     let version = editor.document.version;
-    let position = editor.selection.active;
+
+    // XXX: EJGA: For some reason TS doesn't catch the typing error here,
+    // beware, because this creates many problems once out of the standard
+    // Node-base Language client and object are serialized!
+    let cursor = editor.selection.active;
+    let position = client.code2ProtocolConverter.asPosition(cursor);
     infoPanel.updateFromServer(
       client,
       uri,

diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
@@ -1,5 +1,4 @@
 import {
-  Position,
   Uri,
   WebviewPanel,
   window,
@@ -21,6 +20,8 @@ import {
   ErrorData,
 } from "../lib/types";
 
+import { URI, Position } from "vscode-languageserver-types";
+
 export const goalReq = new RequestType<GoalRequest, GoalAnswer<PpString>, void>(
   "proof/goals"
 );
@@ -144,17 +145,16 @@ export class InfoPanel {
       );
     }
   }
+
+  // Protocol-level data
   updateFromServer(
     client: BaseLanguageClient,
-    uri: Uri,
+    uri: URI,
     version: number,
     position: Position,
     pp_format: "Pp" | "Str"
   ) {
-    let textDocument = VersionedTextDocumentIdentifier.create(
-      uri.toString(),
-      version
-    );
+    let textDocument = VersionedTextDocumentIdentifier.create(uri, version);
 
     // Example to test the `command` parameter
     // let command = "idtac.";

diff --git a/editor/code/src/perf.ts b/editor/code/src/perf.ts
@@ -7,7 +7,7 @@ import {
   window,
 } from "vscode";
 import { NotificationType } from "vscode-languageclient";
-import { DocumentPerfParams } from "../lib/types";
+import { DocumentPerfParams, PerfMessagePayload } from "../lib/types";
 
 export const coqPerfData = new NotificationType<DocumentPerfParams>(
   "$/coq/filePerfData"
@@ -51,11 +51,13 @@ export class PerfDataView implements Disposable {
       </html>`;
 
       this.updateWebView = (params: DocumentPerfParams) => {
-        webview.webview.postMessage({ method: "update", params });
+        let message: PerfMessagePayload = { method: "update", params };
+        webview.webview.postMessage(message);
       };
 
       // We reset spurious old-sessions data
-      webview.webview.postMessage({ method: "reset" });
+      let message: PerfMessagePayload = { method: "reset" };
+      webview.webview.postMessage(message);
     };
     let perfProvider: WebviewViewProvider = { resolveWebviewView };
     this.panel = window.registerWebviewViewProvider(

diff --git a/editor/code/views/info/Loc.tsx b/editor/code/views/info/Loc.tsx
@@ -1,12 +1,15 @@
 import { Loc } from "../../lib/types";
 
 export type LocP = { loc?: Loc };
+
+// Note, this is for display, so we need to adjust for both lines and
+// columns to start at 1, hence the + 1
 export function Loc({ loc }: LocP) {
   if (!loc) return null;
-  let l1 = loc.line_nb + 1;
-  let c1 = loc.bp - loc.bol_pos;
-  let l2 = loc.line_nb_last + 1;
-  let c2 = loc.ep - loc.bol_pos_last;
+  let l1 = loc.line_nb;
+  let c1 = loc.bp - loc.bol_pos + 1;
+  let l2 = loc.line_nb_last;
+  let c2 = loc.ep - loc.bol_pos_last + 1;
 
   return <span>{`l:${l1},c:${c1}--l:${l2},c:${c2}`}</span>;
 }
diff --git a/editor/code/views/perf/App.tsx b/editor/code/views/perf/App.tsx
@@ -7,7 +7,11 @@ import {
 } from "@vscode/webview-ui-toolkit/react";
 import "./media/App.css";
 import { Range } from "vscode-languageserver-types";
-import { DocumentPerfParams } from "../../lib/types";
+import {
+  DocumentPerfParams,
+  PerfMessageEvent,
+  SentencePerfParams,
+} from "../../lib/types";
 
 const vscode: WebviewApi<DocumentPerfParams> = acquireVsCodeApi();
 
@@ -17,9 +21,14 @@ let empty: DocumentPerfParams = {
   timings: [],
 };
 
-let init = vscode.getState() || empty;
+function validOrEmpty(p: DocumentPerfParams | undefined): DocumentPerfParams {
+  // XXX We need to be careful here, when we update the
+  // DocumentPerfParams data type, the saved data here will make the
+  // view crash
+  return empty;
+}
 
-interface CoqMessageEvent extends MessageEvent {}
+let init = validOrEmpty(vscode.getState());
 
 function printWords(w: number) {
   if (w < 1024) {
@@ -31,29 +40,55 @@ function printWords(w: number) {
   }
 }
 
-function SentencePerfCell({ field, value }) {
+// XXX: Would be nice to have typing here, but...
+interface PerfCellP {
+  field: keyof SentencePerfParams | string;
+  value: any;
+}
+
+function SentencePerfCell({ field, value }: PerfCellP) {
   switch (field) {
-    case "loc":
+    case "range":
       let r = value as Range;
       return (
         <span>{`l: ${r.start.line} c: ${r.start.character} -- l: ${r.end.line} c: ${r.end.character}`}</span>
       );
+    case "real":
     case "time":
       return <span>{`${value.toFixed(4).toString()} secs`}</span>;
     case "mem":
       return <span>{printWords(value)}</span>;
+    case "cached":
+      return <span>{value ? "True" : "False"}</span>;
     default:
       return null;
   }
 }
-function SentencePerfRow({ idx, value }) {
+
+interface PerfParamsP {
+  idx: number;
+  value: SentencePerfParams;
+}
+
+function perfFlatten(v: SentencePerfParams) {
+  return {
+    range: v.range,
+    time: v.info.time,
+    real: v.info.real,
+    cached: v.info.cached,
+    mem: v.info.mem,
+  };
+}
+
+function SentencePerfRow({ idx, value }: PerfParamsP) {
+  console.log(value);
   return (
     <VSCodeDataGridRow key={idx + 1}>
       <>
-        {Object.entries(value).map(([field, _value], idx) => {
+        {Object.entries(perfFlatten(value)).map(([field, value], idx) => {
           return (
             <VSCodeDataGridCell key={idx + 1} grid-column={idx + 1}>
-              <SentencePerfCell field={field} value={value[field]} />
+              <SentencePerfCell field={field} value={value} />
             </VSCodeDataGridCell>
           );
         })}
@@ -65,10 +100,11 @@ function SentencePerfRow({ idx, value }) {
 function App() {
   let [perfData, setPerfData] = useState(init);
 
-  function viewDispatch(event: CoqMessageEvent) {
+  function viewDispatch(event: PerfMessageEvent) {
     switch (event.data.method) {
       case "update":
         vscode.setState(event.data.params);
+        // TODO, sort?
         setPerfData(event.data.params);
         break;
       case "reset":
@@ -92,19 +128,19 @@ function App() {
       <VSCodeDataGrid aria-label="Timing Information">
         <VSCodeDataGridRow key={0} rowType="sticky-header">
           <>
-            {Object.entries(perfData.timings[0] ?? []).map(
-              ([field, _value], idx) => {
-                return (
-                  <VSCodeDataGridCell
-                    key={field}
-                    grid-column={idx + 1}
-                    cell-type="columnheader"
-                  >
-                    {field}
-                  </VSCodeDataGridCell>
-                );
-              }
-            )}
+            {Object.entries(
+              perfData.timings[0] ? perfFlatten(perfData.timings[0]) : {}
+            ).map(([field, _value], idx) => {
+              return (
+                <VSCodeDataGridCell
+                  key={field}
+                  grid-column={idx + 1}
+                  cell-type="columnheader"
+                >
+                  {field}
+                </VSCodeDataGridCell>
+              );
+            })}
           </>
         </VSCodeDataGridRow>
         <>

diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md
@@ -302,21 +302,39 @@ when the checking completes, and includes information about execution
 hotspots and memory use by sentences.
 
 ```typescript
+export interface PerfInfo {
+  // Original Execution Time (when not cached)
+  time: number;
+  // Whether the execution was cached
+  cached: boolean;
+  // "Real" Execution Time, often very low for memoized sentences
+  real: number;
+  // Difference in words allocated in the heap using `Gc.quick_stat`
+  mem: number;
+}
+
 export interface SentencePerfParams {
-    loc: Loc,
-    time: number,
-    mem, number
+  range: Range;
+  info: PerfInfo;
 }
 
 export interface DocumentPerfParams {
+  textDocument: VersionedTextDocumentIdentifier;
   summary: string;
   timings: SentencePerfParams[];
 }
-}
 ```
 
 #### Changelog
 
+- v0.1.9:
+  + new server-side option to control whether the notification is sent
+  + the `loc : Loc` field is now `range: Range`
+  + `filePerfData` will send the full document, ordered linearly, in
+    0.1.7 we only sent the top 10 hotspots
+  + `time` and `mem` are now into a better `PerfInfo` data, which
+    correctly provides info for memoized sentences
+- v0.1.8: Spec was accidentally broken
 - v0.1.7: Initial version
 
 ### Trim cache notification

diff --git a/fleche/perf.ml b/fleche/perf.ml
@@ -5,11 +5,21 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-module Sentence = struct
+module Info = struct
   type t =
-    { loc : Lang.Range.t
-    ; time : float
+    { time : float  (** Original Execution Time (when not cached) *)
+    ; cached : bool  (** was the sentence cached? *)
+    ; real : float
+          (** "Real" Execution Time, often very low for memoized sentences *)
     ; mem : float
+          (** Difference in words allocated in the heap using `Gc.quick_stat` *)
+    }
+end
+
+module Sentence = struct
+  type t =
+    { range : Lang.Range.t
+    ; info : Info.t
     }
 end
 

diff --git a/fleche/perf.mli b/fleche/perf.mli
@@ -5,11 +5,21 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-module Sentence : sig
+module Info : sig
   type t =
-    { loc : Lang.Range.t
-    ; time : float
+    { time : float  (** Original Execution Time (when not cached) *)
+    ; cached : bool  (** was the sentence cached? *)
+    ; real : float
+          (** "Real" Execution Time, often very low for memoized sentences *)
     ; mem : float
+          (** Difference in words allocated in the heap using `Gc.quick_stat` *)
+    }
+end
+
+module Sentence : sig
+  type t =
+    { range : Lang.Range.t
+    ; info : Info.t
     }
 end