diff --git a/CHANGES.md b/CHANGES.md index dac06c04a..c4f0bc2f7 100644 --- 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 index 2de1f1150..6f92d3ff9 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -31,6 +31,7 @@ export interface Message { 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 index 302c3842c..81b13204f 100644 --- 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 index c5c81184d..26ac529f4 100644 --- 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, 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 index 34c73f402..d7d4ae6c7 100644 --- 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( "$/coq/filePerfData" @@ -51,11 +51,13 @@ export class PerfDataView implements Disposable { `; 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 index a7d7142a3..56faf4777 100644 --- 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 {`l:${l1},c:${c1}--l:${l2},c:${c2}`}; } diff --git a/editor/code/views/perf/App.tsx b/editor/code/views/perf/App.tsx index 17f59a44b..8441d584a 100644 --- 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 = 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 ( {`l: ${r.start.line} c: ${r.start.character} -- l: ${r.end.line} c: ${r.end.character}`} ); + case "real": case "time": return {`${value.toFixed(4).toString()} secs`}; case "mem": return {printWords(value)}; + case "cached": + return {value ? "True" : "False"}; 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 ( <> - {Object.entries(value).map(([field, _value], idx) => { + {Object.entries(perfFlatten(value)).map(([field, value], idx) => { return ( - + ); })} @@ -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() { <> - {Object.entries(perfData.timings[0] ?? []).map( - ([field, _value], idx) => { - return ( - - {field} - - ); - } - )} + {Object.entries( + perfData.timings[0] ? perfFlatten(perfData.timings[0]) : {} + ).map(([field, _value], idx) => { + return ( + + {field} + + ); + })} <> diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index cc512143a..434b516cf 100644 --- 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 index 346829ac0..2839d8af0 100644 --- 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 index 5e8bb57a3..b918dd09e 100644 --- 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 diff --git a/fleche/perf_analysis.ml b/fleche/perf_analysis.ml index 158c97b0d..7437b12b0 100644 --- a/fleche/perf_analysis.ml +++ b/fleche/perf_analysis.ml @@ -1,14 +1,20 @@ open Perf -let rec list_take n = function +let rec _list_take n = function | [] -> [] - | x :: xs -> if n = 0 then [] else x :: list_take (n - 1) xs + | x :: xs -> if n = 0 then [] else x :: _list_take (n - 1) xs -let mk_loc_time (n : Doc.Node.t) = - let time = Option.default 0.0 n.info.time in +let mk_info (n : Doc.Node.t) = + let time = 0.0 in + let real = Option.default 0.0 n.info.time in + let cached = n.info.cache_hit in let mem = n.info.mw_after -. n.info.mw_prev in - let loc = n.Doc.Node.range in - Sentence.{ loc; time; mem } + Info.{ time; cached; real; mem } + +let mk_sentence (n : Doc.Node.t) = + let range = n.range in + let info = mk_info n in + Sentence.{ range; info } let get_stats ~(doc : Doc.t) = match List.rev doc.nodes with @@ -28,11 +34,12 @@ let make (doc : Doc.t) = Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@\n}" n_stm stats Stats.pp_words cache_size in - let top = - List.stable_sort - (fun (n1 : 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 + (* let top = *) + (* List.stable_sort *) + (* (fun (n1 : 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_sentence top in *) + let timings = List.map mk_sentence doc.nodes in { summary; timings } diff --git a/lsp/jFleche.ml b/lsp/jFleche.ml index 130ae1d96..734d019a0 100644 --- a/lsp/jFleche.ml +++ b/lsp/jFleche.ml @@ -116,6 +116,10 @@ module FlecheDocument = struct [@@deriving yojson] end +module Info = struct + type t = [%import: Fleche.Perf.Info.t] [@@deriving yojson] +end + module SentencePerfData = struct type t = [%import: Fleche.Perf.Sentence.t] [@@deriving yojson] end