Auto restart files with stale dependencies

vscode-lean4/manual/manual.md

@@ -204,6 +204,7 @@ Instead, the state of all dependencies of `Module.lean` needs to be updated manu
 VS Code will display [error- or information-level diagnostics](#errors-warnings-and-information) whenever a dependency of a file is edited and saved. When initially opening a file and a dependency would need to be rebuilt to be up-to-date, it issues an error and refuses to [process](#file-processing) the rest of the file. When a dependency changes while the file is already open, it issues an information-level diagnostic, but will continue processing the file with the previous state of the dependency.
 
 In order to automatically trigger rebuilds of all changed dependencies when opening a file instead of issuing an error, the 'Lean 4: Automatically Build Dependency' setting can be enabled.
+In order to automatically restart an already-open file when Lean reports that its dependencies are out of date, the 'Lean 4: Automatically Restart File On Dependency Change' setting can be enabled.
 
 <br/>
 

vscode-lean4/package.json

@@ -71,6 +71,11 @@
                     "default": false,
                     "markdownDescription": "Enable automatically building dependencies when opening a file. In Lean versions pre-4.2.0, dependencies are always built automatically regardless of this setting."
                 },
+                "lean4.automaticallyRestartFileOnDependencyChange": {
+                    "type": "boolean",
+                    "default": false,
+                    "markdownDescription": "Automatically restart a Lean file when the Lean server reports that its imports are out of date because a dependency changed. This can trigger expensive dependency rebuilds."
+                },
                 "lean4.envPathExtensions": {
                     "type": "array",
                     "default": [],

vscode-lean4/src/config.ts

@@ -17,6 +17,10 @@ export function automaticallyBuildDependencies(): boolean {
     return workspace.getConfiguration('lean4').get('automaticallyBuildDependencies', false)
 }
 
+export function automaticallyRestartFileOnDependencyChange(): boolean {
+    return workspace.getConfiguration('lean4').get('automaticallyRestartFileOnDependencyChange', false)
+}
+
 export function envPathExtensions(): PATH {
     return new PATH(workspace.getConfiguration('lean4').get('envPathExtensions', []))
 }

vscode-lean4/src/leanclient.ts

@@ -41,6 +41,7 @@ import {
 } from '@leanprover/infoview-api'
 import {
     allowedLoggingMethods,
+    automaticallyRestartFileOnDependencyChange,
     disallowedLoggingMethods,
     isLoggingEnabled,
     loggingDir,
@@ -56,6 +57,7 @@ import { DiagnosticChangeEvent, LeanClientDiagnosticCollection } from './diagnos
 import { formatCommandExecutionOutput } from './utils/batch'
 import {
     c2pConverter,
+    LeanDiagnostic,
     LeanImport,
     LeanModule,
     LeanModuleHierarchyImportedByParams,
@@ -107,7 +109,7 @@ interface LeanClientCapabilties {
 const leanClientCapabilities: LeanClientCapabilties = {
     incrementalDiagnosticSupport: true,
     silentDiagnosticSupport: true,
-    rpcWireFormat: 'v1'
+    rpcWireFormat: 'v1',
 }
 
 export type PrepareModuleHierarchyResult =
@@ -136,6 +138,8 @@ export class LeanClient implements Disposable {
     private showingRestartMessage: boolean = false
     private isRestarting: boolean = false
     private staleDepNotifier: Disposable | undefined
+    // Prevent repeatedly restarting a file while the same stale-dependency diagnostic remains active.
+    private autoRestartedStaleDependencyUris: Set<string> = new Set()
     private configFileContents: Map<string, string> = new Map()
 
     private openServerDocuments: Set<string> = new Set<string>()
@@ -549,7 +553,9 @@ export class LeanClient implements Disposable {
             const vsCodeCollection = languages.createDiagnosticCollection('lean4')
             this.diagnosticCollection = new LeanClientDiagnosticCollection(vsCodeCollection)
             this.diagnosticCollection.onDidChangeDiagnostics((e: DiagnosticChangeEvent) => {
-                this.diagnosticsEmitter.fire(e.accumulatedParams())
+                const params = e.accumulatedParams()
+                this.diagnosticsEmitter.fire(params)
+                void this.maybeAutoRestartFileWithStaleDependencies(params)
             })
             this.client.onNotification('textDocument/publishDiagnostics', (params: LeanPublishDiagnosticsParams) => {
                 this.diagnosticCollection?.publishDiagnostics(params)
@@ -621,7 +627,46 @@ export class LeanClient implements Disposable {
         insideRestart = false
     }
 
+    private isStaleDependencyDiagnostic(diagnostic: LeanDiagnostic): boolean {
+        const message = diagnostic.message.toLowerCase()
+        const mentionsRestartFile = message.includes('restart file')
+        const isImportsOutdated = message.includes('imports are out of date')
+        const isDependencyModified = message.includes('dependenc') && message.includes('modified')
+        return mentionsRestartFile && (isImportsOutdated || isDependencyModified)
+    }
+
+    private async maybeAutoRestartFileWithStaleDependencies(params: LeanPublishDiagnosticsParams): Promise<void> {
+        const fileUri = parseExtUri(params.uri)
+        if (fileUri === undefined) {
+            return
+        }
+
+        const uri = fileUri.toString()
+        const hasStaleDependencyDiagnostic = params.diagnostics.some(d => this.isStaleDependencyDiagnostic(d))
+        if (!hasStaleDependencyDiagnostic) {
+            this.autoRestartedStaleDependencyUris.delete(uri)
+            return
+        }
+
+        if (!automaticallyRestartFileOnDependencyChange() || this.autoRestartedStaleDependencyUris.has(uri)) {
+            return
+        }
+
+        const document = lean.getLeanDocumentByUri(fileUri)
+        if (document === undefined) {
+            return
+        }
+
+        this.autoRestartedStaleDependencyUris.add(uri)
+        logger.log(`[LeanClient] Automatically restarting file with stale dependencies: ${uri}`)
+        await this.restartFile(document)
+    }
+
     private checkForImportsOutdatedError(params: LeanPublishDiagnosticsParams) {
+        if (automaticallyRestartFileOnDependencyChange()) {
+            return
+        }
+
         const fileUri = parseExtUri(params.uri)
         if (fileUri === undefined) {
             return
@@ -730,6 +775,7 @@ export class LeanClient implements Disposable {
         this.diagnosticCollection = undefined
         this.client = undefined
         this.openServerDocuments = new Set()
+        this.autoRestartedStaleDependencyUris = new Set()
         this.running = false
     }