[perf] Fixes and improvements towards more interesting uses.

Motivated by the nice heatmap (PR #686) , we fix and improve perf
data, in particular we include data that is cache-aware, and 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)

Co-authored-by: Ali Caglayan <alizter@gmail.com>

CHANGES.md

@@ -99,9 +99,13 @@
  - Update Nix flake enviroment (@Alizter, #684 #688)
  - Update `prettier` (@Alizter @ejgallego, #684 #688)
  - Store original performance data in the cache, so we now display the
-   original timing and memory data even for cached commands (@ejgallego, #)
+   original timing and memory data even for cached commands (@ejgallego, #693)
  - Fix type errors in the Performance Data Notifications (@ejgallego,
-   @Alizter, #)
+   @Alizter, #689, #693)
+ - Send performance performance data for the full document
+   (@ejgallego, @Alizter, #689, #693)
+ - Better types `coq/perfData` call (@ejgallego @Alizter, #689)
+ - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

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,10 +114,20 @@ export interface FlecheSaveParams {
   textDocument: VersionedTextDocumentIdentifier;
 }
 
-export interface SentencePerfParams {
-  Range: Range;
+export interface PerfInfo {
+  // Original Execution Time (when not cached)
   time: number;
+  // Difference in words allocated in the heap using `Gc.quick_stat`
   memory: number;
+  // Whether the execution was cached
+  cache_hit: boolean;
+  // Caching overhead
+  time_hash: number;
+}
+
+export interface SentencePerfParams {
+  range: Range;
+  info: PerfInfo;
 }
 
 export interface DocumentPerfParams {
@@ -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;
+}

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,

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.";

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(

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>;
 }

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,26 @@ let empty: DocumentPerfParams = {
   timings: [],
 };
 
-let init = vscode.getState() || empty;
+function validateViewState(p: DocumentPerfParams) {
+  return (
+    p.textDocument &&
+    p.summary &&
+    p.timings &&
+    p.timings[0] &&
+    p.timings[0].range &&
+    p.timings[0].info
+  );
+}
 
-interface CoqMessageEvent extends MessageEvent {}
+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
+  if (p && validateViewState(p)) return p;
+  else return empty;
+}
+
+let init = validOrEmpty(vscode.getState());
 
 function printWords(w: number) {
   if (w < 1024) {
@@ -31,29 +52,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 "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 "time_hash":
     case "time":
       return <span>{`${value.toFixed(4).toString()} secs`}</span>;
     case "memory":
       return <span>{printWords(value)}</span>;
+    case "cache_hit":
+      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,
+    memory: v.info.memory,
+    cache_hit: v.info.cache_hit,
+    time_hash: v.info.time_hash,
+  };
+}
+
+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>
           );
         })}
@@ -62,13 +109,29 @@ function SentencePerfRow({ idx, value }) {
   );
 }
 
+function timeCmp(t1: SentencePerfParams, t2: SentencePerfParams) {
+  return t2.info.time - t1.info.time;
+}
+
+function viewSort(p: DocumentPerfParams) {
+  let textDocument = p.textDocument;
+  let summary = p.summary;
+  let tlength = p.timings.length;
+  let timings = Array.from(p.timings)
+    .sort(timeCmp)
+    .slice(0, Math.min(30, tlength));
+  return { textDocument, summary, timings };
+}
+
 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);
+        if (!validateViewState(event.data.params)) break;
+        let data = viewSort(event.data.params);
+        vscode.setState(data);
         setPerfData(event.data.params);
         break;
       case "reset":
@@ -92,19 +155,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>
         <>

etc/doc/PROTOCOL.md

@@ -298,32 +298,47 @@ The request will return `null`, or fail if not successful.
 ### Performance Data Notification
 
 The `$/coq/filePerfData` notification is sent from server to client
-when the checking completes, and includes information about execution
-hotspots and memory use by sentences.
+when the checking completes (if the server-side `send_perf_data`
+option is enabled); it includes information about execution hotspots,
+caching, and memory use by sentences:
 
 ```typescript
+export interface PerfInfo {
+  // Original Execution Time (when not cached)
+  time: number;
+  // Difference in words allocated in the heap using `Gc.quick_stat`
+  memory: number;
+  // Whether the execution was cached
+  cache_hit: boolean;
+  // Caching overhead
+  time_hash: number;
+}
+
 export interface SentencePerfParams {
-    range: Range,
-    time: number,
-    memory, 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
   + Fields renamed: `loc -> range`, `mem -> memory`
   + Fixed type for `range`, it was always `Range`
+  + `time` and `memory` are now into a better `PerfInfo` data, which
+    correctly provides info for memoized sentences
   + We now send the real time, even if the command was cached
   + `memory` now means difference in memory from `GC.quick_stat`
-  + we send all the sentences in the document, not only the top 10
-    hotspots, and we send them in document order
+  + `filePerfData` will send the full document, ordered linearly, in
+    0.1.7 we only sent the top 10 hotspots
+- v0.1.8: Spec was accidentally broken, types were invalid
 - v0.1.7: Initial version
 
 ### Trim cache notification

examples/Rtrigo1.v

@@ -116,7 +116,7 @@ Proof.
   2:{ apply pow_nonzero; assumption. }
   unfold Rsqr; ring.
 Qed.
-Definition muuu := 3.
+
 (**********)
 Lemma continuity_cos : continuity cos.
 Proof.