From f751735704e7086a67ac301930062f0c5cc25a51 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Sat, 6 Jul 2024 14:53:55 +0200
Subject: [PATCH] feat: [lean4web] customizable project precondition checks

---
 .../src/diagnostics/setupDiagnostics.ts       | 17 ++++++++
 vscode-lean4/src/extension.ts                 |  7 +++-
 vscode-lean4/src/utils/clientProvider.ts      | 40 +++++++------------
 3 files changed, 37 insertions(+), 27 deletions(-)

diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts
index 37f4cee92..38f982ca1 100644
--- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts
+++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts
@@ -2,6 +2,7 @@ import { SemVer } from 'semver'
 import { OutputChannel, commands } from 'vscode'
 import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi'
 import { LeanInstaller } from '../utils/leanInstaller'
+import { willUseLakeServer } from '../utils/projectInfo'
 import { diagnose } from './setupDiagnoser'
 import {
     PreconditionCheckResult,
@@ -235,3 +236,19 @@ export async function checkIsVSCodeUpToDate(): Promise<PreconditionCheckResult>
             return 'Fulfilled'
     }
 }
+
+export async function checkLean4ProjectPreconditions(
+    channel: OutputChannel,
+    folderUri: ExtUri,
+): Promise<PreconditionCheckResult> {
+    return await checkAll(
+        () => checkIsValidProjectFolder(channel, folderUri),
+        () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: false }),
+        async () => {
+            if (!(await willUseLakeServer(folderUri))) {
+                return 'Fulfilled'
+            }
+            return await checkIsLakeInstalledCorrectly(channel, folderUri, {})
+        },
+    )
+}
diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts
index dcb095753..0e78e0193 100644
--- a/vscode-lean4/src/extension.ts
+++ b/vscode-lean4/src/extension.ts
@@ -11,6 +11,7 @@ import {
     checkIsElanUpToDate,
     checkIsLean4Installed,
     checkIsVSCodeUpToDate,
+    checkLean4ProjectPreconditions,
 } from './diagnostics/setupDiagnostics'
 import { PreconditionCheckResult } from './diagnostics/setupNotifs'
 import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports'
@@ -170,7 +171,11 @@ async function activateLean4Features(
         return undefined
     }
 
-    const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel())
+    const clientProvider = new LeanClientProvider(
+        installer,
+        installer.getOutputChannel(),
+        checkLean4ProjectPreconditions,
+    )
     context.subscriptions.push(clientProvider)
 
     const watchService = new LeanConfigWatchService()
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
index 24212b73f..cb3159c31 100644
--- a/vscode-lean4/src/utils/clientProvider.ts
+++ b/vscode-lean4/src/utils/clientProvider.ts
@@ -1,34 +1,12 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
 import { Disposable, EventEmitter, OutputChannel, TextDocument, commands, window, workspace } from 'vscode'
-import {
-    checkAll,
-    checkIsLakeInstalledCorrectly,
-    checkIsLeanVersionUpToDate,
-    checkIsValidProjectFolder,
-} from '../diagnostics/setupDiagnostics'
 import { PreconditionCheckResult } from '../diagnostics/setupNotifs'
 import { LeanClient } from '../leanclient'
 import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri, toExtUri } from './exturi'
 import { LeanInstaller } from './leanInstaller'
 import { logger } from './logger'
 import { displayError } from './notifs'
-import { findLeanProjectRoot, willUseLakeServer } from './projectInfo'
-
-async function checkLean4ProjectPreconditions(
-    channel: OutputChannel,
-    folderUri: ExtUri,
-): Promise<PreconditionCheckResult> {
-    return await checkAll(
-        () => checkIsValidProjectFolder(channel, folderUri),
-        () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: false }),
-        async () => {
-            if (!(await willUseLakeServer(folderUri))) {
-                return 'Fulfilled'
-            }
-            return await checkIsLakeInstalledCorrectly(channel, folderUri, {})
-        },
-    )
-}
+import { findLeanProjectRoot } from './projectInfo'
 
 // This class ensures we have one LeanClient per folder.
 export class LeanClientProvider implements Disposable {
@@ -53,7 +31,14 @@ export class LeanClientProvider implements Disposable {
     private clientStoppedEmitter = new EventEmitter<[LeanClient, boolean, ServerStoppedReason]>()
     clientStopped = this.clientStoppedEmitter.event
 
-    constructor(installer: LeanInstaller, outputChannel: OutputChannel) {
+    constructor(
+        installer: LeanInstaller,
+        outputChannel: OutputChannel,
+        private checkLean4ProjectPreconditions: (
+            channel: OutputChannel,
+            folderUri: ExtUri,
+        ) => Promise<PreconditionCheckResult>,
+    ) {
         this.outputChannel = outputChannel
         this.installer = installer
 
@@ -122,7 +107,10 @@ export class LeanClientProvider implements Disposable {
                     continue
                 }
 
-                const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, projectUri)
+                const preconditionCheckResult = await this.checkLean4ProjectPreconditions(
+                    this.outputChannel,
+                    projectUri,
+                )
                 if (preconditionCheckResult !== 'Fatal') {
                     logger.log('[ClientProvider] got lean version 4')
                     const [cached, client] = await this.ensureClient(uri)
@@ -234,7 +222,7 @@ export class LeanClientProvider implements Disposable {
         }
         this.pending.set(key, true)
 
-        const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, folderUri)
+        const preconditionCheckResult = await this.checkLean4ProjectPreconditions(this.outputChannel, folderUri)
         if (preconditionCheckResult === 'Fatal') {
             this.pending.delete(key)
             return [false, undefined]