test: logging

Author: mhuisi

vscode-lean4/src/infoview.ts

@@ -212,17 +212,27 @@ export class InfoProvider implements Disposable {
                 }
                 const id = this.freshClientRequestId
                 this.freshClientRequestId += 1
-                const promise = client.sendRequest(method, params, tk.token).catch(async ex => {
-                    if (ex.code === RpcErrorCode.WorkerCrashed) {
-                        // ex codes related with worker exited or crashed
-                        logger.log(`[InfoProvider]The Lean Server has stopped processing this file: ${ex.message}`)
-                        await this.onWorkerStopped(uri, client, {
-                            message: 'The Lean Server has stopped processing this file: ',
-                            reason: ex.message as string,
-                        })
-                    }
-                    throw ex
-                })
+                logger.log(`[InfoProvider][trace] startClientRequest id=${id} method=${method} uri=${uri}`)
+                const promise = client
+                    .sendRequest(method, params, tk.token)
+                    .then(res => {
+                        logger.log(`[InfoProvider][trace] startClientRequest id=${id} resolved`)
+                        return res
+                    })
+                    .catch(async ex => {
+                        logger.log(
+                            `[InfoProvider][trace] startClientRequest id=${id} rejected code=${ex?.code} msg=${ex?.message}`,
+                        )
+                        if (ex.code === RpcErrorCode.WorkerCrashed) {
+                            // ex codes related with worker exited or crashed
+                            logger.log(`[InfoProvider]The Lean Server has stopped processing this file: ${ex.message}`)
+                            await this.onWorkerStopped(uri, client, {
+                                message: 'The Lean Server has stopped processing this file: ',
+                                reason: ex.message as string,
+                            })
+                        }
+                        throw ex
+                    })
                 this.clientRequests.set(id, [promise, sub, tk])
                 return id
             }
@@ -691,6 +701,7 @@ export class InfoProvider implements Disposable {
     }
 
     async onWorkerStopped(uri: string, client: LeanClient, reason: ServerStoppedReason) {
+        logger.log(`[InfoProvider][trace] onWorkerStopped uri=${uri} reason=${reason.reason}`)
         await this.webviewPanel?.api.serverStopped(reason)
 
         const extUri = parseExtUri(uri)
@@ -978,10 +989,14 @@ export class InfoProvider implements Disposable {
     private async sendPosition() {
         const editor = lean.activeLeanEditor
         if (editor === undefined) {
+            logger.log('[InfoProvider][trace] sendPosition skipped: no active lean editor')
             return
         }
         const loc = this.getLocation(editor)
         const uri = editor.documentExtUri
+        logger.log(
+            `[InfoProvider][trace] sendPosition uri=${uri.toString()} clientsFailed=${this.clientsFailed.size} workersFailed=${this.workersFailed.size}`,
+        )
         if (this.clientsFailed.size > 0 || this.workersFailed.size > 0) {
             const client = this.clientProvider.findClient(uri)
             const uriKey = uri.toString()

vscode-lean4/src/leanclient.ts

@@ -570,6 +570,8 @@ export class LeanClient implements Disposable {
                 const params = params_ as LeanFileProgressParams
                 const uri = toExtUri(p2cConverter.asUri(params.textDocument.uri))
                 if (uri !== undefined) {
+                    const kinds = (params.processing as any[]).map(p => p.kind).join(',')
+                    logger.log(`[LeanClient][trace] fileProgress uri=${uri.toString()} kinds=[${kinds}]`)
                     this.progressChangedEmitter.fire([uri.toString(), params.processing])
                     // save the latest progress on this Uri in case infoview needs it later.
                     this.progress.set(uri, params.processing)