Fix critical issue with diagnostics in CoqProofChecker

Author: K-dizzled

src/coqLsp/coqLspClient.ts

@@ -189,6 +189,7 @@ export class CoqLspClient implements CoqLspClientInterface {
         requestType: ProtocolNotificationType<any, any>,
         params: any,
         uri: Uri,
+        version: number,
         lastDocumentEndPosition?: Position,
         timeout: number = 300000
     ): Promise<DiagnosticMessage> {
@@ -210,7 +211,10 @@ export class CoqLspClient implements CoqLspClientInterface {
             this.client.onNotification(
                 PublishDiagnosticsNotification.type,
                 (params) => {
-                    if (params.uri.toString() === uri.uri) {
+                    if (
+                        params.uri.toString() === uri.uri &&
+                        params.version === version
+                    ) {
                         pendingDiagnostic = false;
                         awaitedDiagnostics = params.diagnostics;
 
@@ -242,6 +246,8 @@ export class CoqLspClient implements CoqLspClientInterface {
             throw new CoqLspError("coq-lsp did not respond in time");
         }
 
+        this.subscriptions.forEach((d) => d.dispose());
+
         return this.filterDiagnostics(
             awaitedDiagnostics,
             lastDocumentEndPosition ?? Position.create(0, 0)
@@ -266,7 +272,8 @@ export class CoqLspClient implements CoqLspClientInterface {
         return await this.waitUntilFileFullyChecked(
             DidOpenTextDocumentNotification.type,
             params,
-            uri
+            uri,
+            version
         );
     }
 
@@ -302,6 +309,7 @@ export class CoqLspClient implements CoqLspClientInterface {
             DidChangeTextDocumentNotification.type,
             params,
             uri,
+            version,
             oldEndPosition
         );
     }

src/core/coqProofChecker.ts

@@ -126,7 +126,6 @@ export class CoqProofChecker implements CoqProofCheckerInterface {
                 auxFileVersion += 1;
                 // 3.2. Append the proof the end of the aux file
                 appendFileSync(auxFileUri.fsPath, proof);
-
                 // 3.3. Issue update text request
                 const diagnosticMessage =
                     await this.coqLspClient.updateTextDocument(
@@ -145,6 +144,15 @@ export class CoqProofChecker implements CoqProofCheckerInterface {
 
                 // 3.5. Bring file to the previous state
                 writeFileSync(auxFileUri.fsPath, sourceFileContent);
+
+                // 3.6. Issue update text request
+                auxFileVersion += 1;
+                await this.coqLspClient.updateTextDocument(
+                    sourceFileContentPrefix,
+                    "",
+                    auxFileUri,
+                    auxFileVersion
+                );
             }
         } finally {
             // 4. Issue close text document request