feat: [lean4web] customizable project precondition checks

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, {})
+ },
+ )
+}

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()

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]