From 9b9f670371a59f059d878021b5f57ef5da87a571 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 17 Jul 2024 15:40:16 -0700 Subject: [PATCH] MVP --- client/package-lock.json | 252 +++++++++++++++++++++++++++++++ client/package.json | 1 + client/src/extension.ts | 12 +- server/src/fstarLspExtensions.ts | 17 ++- server/src/server.ts | 18 ++- 5 files changed, 294 insertions(+), 6 deletions(-) diff --git a/client/package-lock.json b/client/package-lock.json index 87272a7..ca67f1c 100644 --- a/client/package-lock.json +++ b/client/package-lock.json @@ -9,6 +9,7 @@ "version": "0.0.2", "license": "MIT", "dependencies": { + "@vscode/extension-telemetry": "^0.9.6", "vscode-languageclient": "^9.0.1" }, "devDependencies": { @@ -19,6 +20,120 @@ "vscode": "^1.86.0" } }, + "node_modules/@microsoft/1ds-core-js": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/1ds-core-js/-/1ds-core-js-4.3.0.tgz", + "integrity": "sha512-0aP0ko4j0E2HfMNG1TdctGxcX74c4nQMMMV2JyaBYRRlbg1qYSVCUTZO4Ap6Qf65cBjJUCoIzgDMXNSquANwDA==", + "dependencies": { + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "node_modules/@microsoft/1ds-post-js": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/1ds-post-js/-/1ds-post-js-4.3.0.tgz", + "integrity": "sha512-a1AflEuB313mfRiNNqkoVYDi4zxnG57zR8KotudtVoov6hiByBIS0KSuf3oE5/woDHWi9ZJjiCDvFwNqNH0YYw==", + "dependencies": { + "@microsoft/1ds-core-js": "4.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "node_modules/@microsoft/applicationinsights-channel-js": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-channel-js/-/applicationinsights-channel-js-3.3.0.tgz", + "integrity": "sha512-xlxcfwgFgvHoY/STVgtRoUSvAKOMNbe4CIBeY8zTHsjE9x3/kY9R9kpRkTBectuD7xVm1/FmzrzqaxcJO7R/sw==", + "dependencies": { + "@microsoft/applicationinsights-common": "3.3.0", + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + }, + "peerDependencies": { + "tslib": "*" + } + }, + "node_modules/@microsoft/applicationinsights-common": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-common/-/applicationinsights-common-3.3.0.tgz", + "integrity": "sha512-5t6WtL9wCQUA06sioaTenz5qWgrCk7QRm99pDuP+vyjcAiT6//f+Qn1K9KXtEX5WfEMHx3vBIDGLl6ppnF1YAQ==", + "dependencies": { + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + }, + "peerDependencies": { + "tslib": "*" + } + }, + "node_modules/@microsoft/applicationinsights-core-js": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-core-js/-/applicationinsights-core-js-3.3.0.tgz", + "integrity": "sha512-so0fFTqgZMjClH+MsiRYGspo5fpgwHEUYNMjyzpf9rjrY7FaUH8kkWzrQ3V0Cs4axZwf+WuIndtDOAws7aBmGQ==", + "dependencies": { + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + }, + "peerDependencies": { + "tslib": "*" + } + }, + "node_modules/@microsoft/applicationinsights-shims": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-shims/-/applicationinsights-shims-3.0.1.tgz", + "integrity": "sha512-DKwboF47H1nb33rSUfjqI6ryX29v+2QWcTrRvcQDA32AZr5Ilkr7whOOSsD1aBzwqX0RJEIP1Z81jfE3NBm/Lg==", + "dependencies": { + "@nevware21/ts-utils": ">= 0.9.4 < 2.x" + } + }, + "node_modules/@microsoft/applicationinsights-web-basic": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-web-basic/-/applicationinsights-web-basic-3.3.0.tgz", + "integrity": "sha512-8+QcrgensCK44XuHMkW+zQXYchM6/f5gg0go/REVj5DpbE03L3jXNajSlBIALH8MzhGgcyPDlGmIt2OYztUMNQ==", + "dependencies": { + "@microsoft/applicationinsights-channel-js": "3.3.0", + "@microsoft/applicationinsights-common": "3.3.0", + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + }, + "peerDependencies": { + "tslib": "*" + } + }, + "node_modules/@microsoft/dynamicproto-js": { + "version": "2.0.3", + "resolved": "https://registry.npmjs.org/@microsoft/dynamicproto-js/-/dynamicproto-js-2.0.3.tgz", + "integrity": "sha512-JTWTU80rMy3mdxOjjpaiDQsTLZ6YSGGqsjURsY6AUQtIj0udlF/jYmhdLZu8693ZIC0T1IwYnFa0+QeiMnziBA==", + "dependencies": { + "@nevware21/ts-utils": ">= 0.10.4 < 2.x" + } + }, + "node_modules/@nevware21/ts-async": { + "version": "0.5.2", + "resolved": "https://registry.npmjs.org/@nevware21/ts-async/-/ts-async-0.5.2.tgz", + "integrity": "sha512-Zf2vUNjCw2vJsiVKhWXA9hCNHsn59AOSGa5jGP4tWrp/vTH9XrI4eG/65khuoAgrS83migj0Xv5/j6fUAz69Zw==", + "dependencies": { + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "node_modules/@nevware21/ts-utils": { + "version": "0.11.3", + "resolved": "https://registry.npmjs.org/@nevware21/ts-utils/-/ts-utils-0.11.3.tgz", + "integrity": "sha512-oipW+tyKN68bREjoESYAzOZiatM+1LF+ez1TX3BaeinhCkI18xsLgmpH9tvwHaVgKf1Tsth25sdbXVtYmgRYvQ==" + }, "node_modules/@tootallnate/once": { "version": "1.1.2", "resolved": "https://registry.npmjs.org/@tootallnate/once/-/once-1.1.2.tgz", @@ -34,6 +149,19 @@ "integrity": "sha512-rWY+Bs6j/f1lvr8jqZTyp5arRMfovdxolcqGi+//+cPDOh8SBvzXH90e7BiSXct5HJ9HGW6jATchbRTpTJpEkw==", "dev": true }, + "node_modules/@vscode/extension-telemetry": { + "version": "0.9.6", + "resolved": "https://registry.npmjs.org/@vscode/extension-telemetry/-/extension-telemetry-0.9.6.tgz", + "integrity": "sha512-qWK2GNw+b69QRYpjuNM9g3JKToMICoNIdc0rQMtvb4gIG9vKKCZCVCz+ZOx6XM/YlfWAyuPiyxcjIY0xyF+Djg==", + "dependencies": { + "@microsoft/1ds-core-js": "^4.1.2", + "@microsoft/1ds-post-js": "^4.1.2", + "@microsoft/applicationinsights-web-basic": "^3.1.2" + }, + "engines": { + "vscode": "^1.75.0" + } + }, "node_modules/@vscode/test-electron": { "version": "2.3.9", "resolved": "https://registry.npmjs.org/@vscode/test-electron/-/test-electron-2.3.9.tgz", @@ -253,6 +381,12 @@ "safe-buffer": "~5.1.0" } }, + "node_modules/tslib": { + "version": "2.6.3", + "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.6.3.tgz", + "integrity": "sha512-xNvxJEOUiWPGhUuUdQgAJPKOOJfGnIyKySOc09XkKsgdUV/3E2zvwZYdejjmRgPCgcym1juLH3226yA7sEFJKQ==", + "peer": true + }, "node_modules/util-deprecate": { "version": "1.0.2", "resolved": "https://registry.npmjs.org/util-deprecate/-/util-deprecate-1.0.2.tgz", @@ -301,6 +435,108 @@ } }, "dependencies": { + "@microsoft/1ds-core-js": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/1ds-core-js/-/1ds-core-js-4.3.0.tgz", + "integrity": "sha512-0aP0ko4j0E2HfMNG1TdctGxcX74c4nQMMMV2JyaBYRRlbg1qYSVCUTZO4Ap6Qf65cBjJUCoIzgDMXNSquANwDA==", + "requires": { + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@microsoft/1ds-post-js": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/1ds-post-js/-/1ds-post-js-4.3.0.tgz", + "integrity": "sha512-a1AflEuB313mfRiNNqkoVYDi4zxnG57zR8KotudtVoov6hiByBIS0KSuf3oE5/woDHWi9ZJjiCDvFwNqNH0YYw==", + "requires": { + "@microsoft/1ds-core-js": "4.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@microsoft/applicationinsights-channel-js": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-channel-js/-/applicationinsights-channel-js-3.3.0.tgz", + "integrity": "sha512-xlxcfwgFgvHoY/STVgtRoUSvAKOMNbe4CIBeY8zTHsjE9x3/kY9R9kpRkTBectuD7xVm1/FmzrzqaxcJO7R/sw==", + "requires": { + "@microsoft/applicationinsights-common": "3.3.0", + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@microsoft/applicationinsights-common": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-common/-/applicationinsights-common-3.3.0.tgz", + "integrity": "sha512-5t6WtL9wCQUA06sioaTenz5qWgrCk7QRm99pDuP+vyjcAiT6//f+Qn1K9KXtEX5WfEMHx3vBIDGLl6ppnF1YAQ==", + "requires": { + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@microsoft/applicationinsights-core-js": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-core-js/-/applicationinsights-core-js-3.3.0.tgz", + "integrity": "sha512-so0fFTqgZMjClH+MsiRYGspo5fpgwHEUYNMjyzpf9rjrY7FaUH8kkWzrQ3V0Cs4axZwf+WuIndtDOAws7aBmGQ==", + "requires": { + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@microsoft/applicationinsights-shims": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-shims/-/applicationinsights-shims-3.0.1.tgz", + "integrity": "sha512-DKwboF47H1nb33rSUfjqI6ryX29v+2QWcTrRvcQDA32AZr5Ilkr7whOOSsD1aBzwqX0RJEIP1Z81jfE3NBm/Lg==", + "requires": { + "@nevware21/ts-utils": ">= 0.9.4 < 2.x" + } + }, + "@microsoft/applicationinsights-web-basic": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@microsoft/applicationinsights-web-basic/-/applicationinsights-web-basic-3.3.0.tgz", + "integrity": "sha512-8+QcrgensCK44XuHMkW+zQXYchM6/f5gg0go/REVj5DpbE03L3jXNajSlBIALH8MzhGgcyPDlGmIt2OYztUMNQ==", + "requires": { + "@microsoft/applicationinsights-channel-js": "3.3.0", + "@microsoft/applicationinsights-common": "3.3.0", + "@microsoft/applicationinsights-core-js": "3.3.0", + "@microsoft/applicationinsights-shims": "3.0.1", + "@microsoft/dynamicproto-js": "^2.0.3", + "@nevware21/ts-async": ">= 0.5.2 < 2.x", + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@microsoft/dynamicproto-js": { + "version": "2.0.3", + "resolved": "https://registry.npmjs.org/@microsoft/dynamicproto-js/-/dynamicproto-js-2.0.3.tgz", + "integrity": "sha512-JTWTU80rMy3mdxOjjpaiDQsTLZ6YSGGqsjURsY6AUQtIj0udlF/jYmhdLZu8693ZIC0T1IwYnFa0+QeiMnziBA==", + "requires": { + "@nevware21/ts-utils": ">= 0.10.4 < 2.x" + } + }, + "@nevware21/ts-async": { + "version": "0.5.2", + "resolved": "https://registry.npmjs.org/@nevware21/ts-async/-/ts-async-0.5.2.tgz", + "integrity": "sha512-Zf2vUNjCw2vJsiVKhWXA9hCNHsn59AOSGa5jGP4tWrp/vTH9XrI4eG/65khuoAgrS83migj0Xv5/j6fUAz69Zw==", + "requires": { + "@nevware21/ts-utils": ">= 0.11.3 < 2.x" + } + }, + "@nevware21/ts-utils": { + "version": "0.11.3", + "resolved": "https://registry.npmjs.org/@nevware21/ts-utils/-/ts-utils-0.11.3.tgz", + "integrity": "sha512-oipW+tyKN68bREjoESYAzOZiatM+1LF+ez1TX3BaeinhCkI18xsLgmpH9tvwHaVgKf1Tsth25sdbXVtYmgRYvQ==" + }, "@tootallnate/once": { "version": "1.1.2", "resolved": "https://registry.npmjs.org/@tootallnate/once/-/once-1.1.2.tgz", @@ -313,6 +549,16 @@ "integrity": "sha512-rWY+Bs6j/f1lvr8jqZTyp5arRMfovdxolcqGi+//+cPDOh8SBvzXH90e7BiSXct5HJ9HGW6jATchbRTpTJpEkw==", "dev": true }, + "@vscode/extension-telemetry": { + "version": "0.9.6", + "resolved": "https://registry.npmjs.org/@vscode/extension-telemetry/-/extension-telemetry-0.9.6.tgz", + "integrity": "sha512-qWK2GNw+b69QRYpjuNM9g3JKToMICoNIdc0rQMtvb4gIG9vKKCZCVCz+ZOx6XM/YlfWAyuPiyxcjIY0xyF+Djg==", + "requires": { + "@microsoft/1ds-core-js": "^4.1.2", + "@microsoft/1ds-post-js": "^4.1.2", + "@microsoft/applicationinsights-web-basic": "^3.1.2" + } + }, "@vscode/test-electron": { "version": "2.3.9", "resolved": "https://registry.npmjs.org/@vscode/test-electron/-/test-electron-2.3.9.tgz", @@ -502,6 +748,12 @@ "safe-buffer": "~5.1.0" } }, + "tslib": { + "version": "2.6.3", + "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.6.3.tgz", + "integrity": "sha512-xNvxJEOUiWPGhUuUdQgAJPKOOJfGnIyKySOc09XkKsgdUV/3E2zvwZYdejjmRgPCgcym1juLH3226yA7sEFJKQ==", + "peer": true + }, "util-deprecate": { "version": "1.0.2", "resolved": "https://registry.npmjs.org/util-deprecate/-/util-deprecate-1.0.2.tgz", diff --git a/client/package.json b/client/package.json index 979e81a..d82d95b 100644 --- a/client/package.json +++ b/client/package.json @@ -16,6 +16,7 @@ "compile": "esbuild --bundle src/extension.ts --outfile=out/extension.js --tsconfig=tsconfig.json --platform=node --external:vscode --sourcemap --preserve-symlinks --sources-content=false" }, "dependencies": { + "@vscode/extension-telemetry": "^0.9.6", "vscode-languageclient": "^9.0.1" }, "devDependencies": { diff --git a/client/src/extension.ts b/client/src/extension.ts index d94ace9..259cb48 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -14,7 +14,8 @@ import { Range, Position } from 'vscode-languageclient/node'; -import { StatusNotificationParams, killAllNotification, killAndRestartSolverNotification, restartNotification, statusNotification, verifyToPositionNotification } from './fstarLspExtensions'; +import { StatusNotificationParams, killAllNotification, killAndRestartSolverNotification, restartNotification, statusNotification, telemetryNotification, verifyToPositionNotification } from './fstarLspExtensions'; +import TelemetryReporter from '@vscode/extension-telemetry'; let client: LanguageClient; @@ -132,6 +133,12 @@ function updateDecorations() { } export async function activate(context: ExtensionContext) { + const telemetry = new TelemetryReporter( + // '160d3440-45e8-47c1-9cf1-ccd46149ff89' + 'InstrumentationKey=160d3440-45e8-47c1-9cf1-ccd46149ff89;IngestionEndpoint=https://eastus-8.in.applicationinsights.azure.com/;LiveEndpoint=https://eastus.livediagnostics.monitor.azure.com/;ApplicationId=a4e6ffa7-4f8c-47c3-8d7f-0f4dbcf57019' + ); + telemetry.sendTelemetryEvent('test', {test:'test'}); + // The server is implemented in node const serverModule = context.asAbsolutePath( path.join('server', 'out', 'main.js') @@ -165,6 +172,9 @@ export async function activate(context: ExtensionContext) { client.onNotification(statusNotification, status => handleStatus(status)); vscode.window.onDidChangeVisibleTextEditors(() => updateDecorations()); + client.onNotification(telemetryNotification, params => + telemetry.sendTelemetryEvent(params.eventName, params.properties, params.measurements)); + // register a command for Ctrl+. context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/verify-to-position', textEditor => client.sendNotification(verifyToPositionNotification, { diff --git a/server/src/fstarLspExtensions.ts b/server/src/fstarLspExtensions.ts index 8bf7dff..c98bbea 100644 --- a/server/src/fstarLspExtensions.ts +++ b/server/src/fstarLspExtensions.ts @@ -45,4 +45,19 @@ export interface VerifyToPositionParams { export const verifyToPositionNotification = new ProtocolNotificationType('$/fstar/verifyToPosition'); -interface RegistrationParams {} \ No newline at end of file +interface RegistrationParams {} + +export interface TelemetryEventProperties { + readonly [key: string]: string | undefined + | any; //apparently we need the safe type here?? +} +export interface TelemetryEventMeasurements { + readonly [key: string]: number | undefined; +} +export interface TelemetryNotificationParams { + eventName: string; + properties?: TelemetryEventProperties; + measurements?: TelemetryEventMeasurements; +} +export const telemetryNotification = + new ProtocolNotificationType('$/fstar/telemetry'); \ No newline at end of file diff --git a/server/src/server.ts b/server/src/server.ts index f9f5bc3..f6c7fbc 100644 --- a/server/src/server.ts +++ b/server/src/server.ts @@ -37,7 +37,7 @@ import { FStar, FStarConfig } from './fstar'; import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse, FStarPosition, FullBufferQuery } from './fstar_messages'; import * as path from 'path'; import { pathToFileURL } from 'url'; -import { statusNotification, FragmentStatus, killAndRestartSolverNotification, restartNotification, verifyToPositionNotification, killAllNotification } from './fstarLspExtensions'; +import { statusNotification, FragmentStatus, killAndRestartSolverNotification, restartNotification, verifyToPositionNotification, killAllNotification, TelemetryEventProperties, TelemetryEventMeasurements } from './fstarLspExtensions'; import { Debouncer, RateLimiter } from './signals'; // LSP Server @@ -72,14 +72,17 @@ export class Server { // * spawn 2 fstar processes: one for typechecking, one lax process for fly-checking and symbol lookup // * set event handlers to read the output of the fstar processes // * send the current document to both processes to start typechecking - this.documents.onDidOpen(ev => - this.onOpenHandler(ev.document) + this.documents.onDidOpen(ev => { + this.sendTelemetryEvent('fstarOpen', {fileName: ev.document.uri, contents: ev.document.getText()}); + return this.onOpenHandler(ev.document) .catch(err => this.connection.window.showErrorMessage( `${URI.parse(ev.document.uri).fsPath}: ${err.toString()}`)) - .catch()); + .catch(); + }); // Only keep settings for open documents this.documents.onDidClose(e => { + this.sendTelemetryEvent('fstarClose', {fileName: e.document.uri, contents: e.document.getText()}); this.documentStates.get(e.document.uri)?.dispose(); this.documentStates.delete(e.document.uri); }); @@ -122,6 +125,7 @@ export class Server { // Custom events this.connection.onNotification(verifyToPositionNotification, ({uri, position, lax}) => { + this.sendTelemetryEvent('fstarVerifyToPosition', { uri, lax, position }); const state = this.getDocumentState(uri); if (lax) { state?.laxToPosition(position); @@ -137,6 +141,10 @@ export class Server { this.onKillAllRequest()); } + sendTelemetryEvent(eventName: string, properties?: TelemetryEventProperties, measurements?: TelemetryEventMeasurements) { + + } + run() { // Make the text document manager listen on the connection // for open, change and close text document events @@ -410,6 +418,7 @@ export class DocumentState { .map(diag => ({...diag, source: 'F* flycheck', ...(diag.severity === DiagnosticSeverity.Error && { severity: DiagnosticSeverity.Warning })}))); } + this.server.sendTelemetryEvent('fstarDiagnostics', { uri: this.uri, diagnostics: diags }); void this.server.connection.sendDiagnostics({ uri: this.uri, diagnostics: diags, @@ -444,6 +453,7 @@ export class DocumentState { }); } + this.server.sendTelemetryEvent('fstarProgress', { uri: this.uri, fragments: statusFragments }); void this.server.connection.sendNotification(statusNotification, { uri: this.uri, fragments: statusFragments,