feat: error when opening project that contains lakefile but no lean-toolchain (#610)

This PR ensures that an error is displayed when users open a project
that has a lakefile but no lean-toolchain file.

Author: mhuisi

vscode-lean4/src/diagnostics/fullDiagnostics.ts

@@ -1,11 +1,11 @@
 import { SemVer } from 'semver'
-import { Disposable, OutputChannel, commands, env } from 'vscode'
+import { commands, Disposable, env, OutputChannel } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from '../utils/batch'
 import { ElanInstalledToolchain, ElanToolchains, ElanUnresolvedToolchain } from '../utils/elan'
-import { FileUri } from '../utils/exturi'
+import { extUriToCwdUri, FileUri } from '../utils/exturi'
 import { lean } from '../utils/leanEditorProvider'
 import { displayNotification, displayNotificationWithInput } from '../utils/notifs'
-import { findLeanProjectRoot } from '../utils/projectInfo'
+import { findLeanProjectRootInfo } from '../utils/projectInfo'
 import {
     ElanDumpStateWithoutNetQueryResult,
     ElanVersionDiagnosis,
@@ -228,17 +228,25 @@ export class FullDiagnosticsProvider implements Disposable {
         // in which case we still want to provide adequate diagnostics. Hence, we use the last active Lean document,
         // regardless of whether there is an actual `LeanClient` managing it.
         const lastActiveLeanDocumentUri = lean.lastActiveLeanDocument?.extUri
-        const projectUri =
-            lastActiveLeanDocumentUri !== undefined && lastActiveLeanDocumentUri.scheme === 'file'
-                ? await findLeanProjectRoot(lastActiveLeanDocumentUri)
+        const projectInfo =
+            lastActiveLeanDocumentUri !== undefined
+                ? await findLeanProjectRootInfo(lastActiveLeanDocumentUri)
                 : undefined
-        if (projectUri === 'FileNotFound') {
+        if (projectInfo?.kind === 'FileNotFound') {
             displayNotification(
                 'Error',
                 `Cannot display setup information for file that does not exist in the file system: ${lastActiveLeanDocumentUri}. Please choose a different file to display the setup information for.`,
             )
             return
         }
+        if (projectInfo?.kind === 'LakefileWithoutToolchain') {
+            displayNotification(
+                'Error',
+                `Cannot display setup information for file in invalid project: Project at ${projectInfo.projectRootUri} has a Lakefile, but no 'lean-toolchain' file. Please create one with the Lean version that you would like the project to use.`,
+            )
+            return
+        }
+        const projectUri = projectInfo !== undefined ? extUriToCwdUri(projectInfo.projectRootUri) : undefined
         const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri)
         const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics)
         const copyToClipboardInput = 'Copy to Clipboard'

vscode-lean4/src/diagnostics/setupDiagnostics.ts

@@ -1,4 +1,3 @@
-import path from 'path'
 import { SemVer } from 'semver'
 import { OutputChannel, commands } from 'vscode'
 import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi'
@@ -39,15 +38,15 @@ const oldServerFolderContainsNewServerFolderErrorMessage = (
     fileUri: FileUri,
     clientFolderUri: FileUri,
 ) =>
-    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${path.basename(fileUri.fsPath)}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running.
+    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running.
 The Lean 4 VS Code extension does not support nested Lean projects.`
 
 const newServerFolderContainsOldServerFolderErrorMessage = (
     folderUri: FileUri,
     fileUri: FileUri,
     clientFolderUri: FileUri,
 ) =>
-    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${path.basename(fileUri.fsPath)}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running.
+    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running.
 The Lean 4 VS Code extension does not support nested Lean projects.`
 
 export class SetupDiagnostics {

vscode-lean4/src/extension.ts

@@ -21,10 +21,10 @@ import { LeanConfigWatchService } from './utils/configwatchservice'
 import { ElanCommandProvider } from './utils/elanCommands'
 import { PATH, setProcessEnvPATH } from './utils/envPath'
 import { onEventWhile, withoutReentrancy } from './utils/events'
-import { FileUri } from './utils/exturi'
+import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi'
 import { displayInternalErrorsIn } from './utils/internalErrors'
 import { registerLeanCommandRunner } from './utils/leanCmdRunner'
-import { lean, LeanEditor, registerLeanEditorProvider } from './utils/leanEditorProvider'
+import { lean, registerLeanEditorProvider } from './utils/leanEditorProvider'
 import { LeanInstaller } from './utils/leanInstaller'
 import {
     displayActiveStickyNotification,
@@ -33,37 +33,28 @@ import {
     setStickyNotificationActiveButHidden,
 } from './utils/notifs'
 import { PathExtensionProvider } from './utils/pathExtensionProvider'
-import { findLeanProjectRoot } from './utils/projectInfo'
+import { findLeanProjectRootInfo } from './utils/projectInfo'
 import { UriHandlerService } from './utils/uriHandlerService'
 
 async function setLeanFeatureSetActive(isActive: boolean) {
     await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive)
 }
 
-async function findLeanEditorProjectUri(editor: LeanEditor): Promise<FileUri | undefined | 'InvalidProject'> {
-    const docUri = editor.documentExtUri
-    const projectUri = docUri.scheme === 'file' ? await findLeanProjectRoot(docUri) : undefined
-    if (projectUri === 'FileNotFound') {
-        return 'InvalidProject'
-    }
-    return projectUri
-}
-
-async function findOpenLeanProjectUri(): Promise<FileUri | undefined | 'NoValidDocument'> {
+async function findOpenLeanProjectUri(): Promise<ExtUri | 'NoValidDocument'> {
     const activeEditor = lean.activeLeanEditor
     if (activeEditor !== undefined) {
-        const projectUri = await findLeanEditorProjectUri(activeEditor)
-        if (projectUri !== 'InvalidProject') {
-            return projectUri
+        const info = await findLeanProjectRootInfo(activeEditor.documentExtUri)
+        if (info.kind !== 'FileNotFound') {
+            return info.projectRootUri
         }
     }
 
     // This happens if vscode starts with a lean file open
     // but the "Getting Started" page is active.
     for (const editor of lean.visibleLeanEditors) {
-        const projectUri = await findLeanEditorProjectUri(editor)
-        if (projectUri !== 'InvalidProject') {
-            return projectUri
+        const info = await findLeanProjectRootInfo(editor.documentExtUri)
+        if (info.kind !== 'FileNotFound') {
+            return info.projectRootUri
         }
     }
 
@@ -220,12 +211,12 @@ async function tryActivatingLean4FeaturesInProject(
     elanCommandProvider: ElanCommandProvider,
     resolve: (value: Lean4EnabledFeatures) => void,
     d: SetupDiagnostics,
-    projectUri: FileUri | undefined,
+    projectUri: ExtUri,
 ) {
     const preconditionCheckResult = await checkLean4FeaturePreconditions(
         installer,
         'Activate Lean 4 Extension',
-        projectUri,
+        extUriToCwdUri(projectUri),
         d,
     )
     if (preconditionCheckResult === 'Fatal') {
@@ -260,8 +251,8 @@ async function tryActivatingLean4Features(
         onEventWhile(
             lean.onDidRevealLeanEditor,
             withoutReentrancy('Continue', async editor => {
-                const projectUri = await findLeanEditorProjectUri(editor)
-                if (projectUri === 'InvalidProject') {
+                const info = await findLeanProjectRootInfo(editor.documentExtUri)
+                if (info.kind === 'FileNotFound') {
                     return 'Continue'
                 }
                 await tryActivatingLean4FeaturesInProject(
@@ -270,7 +261,7 @@ async function tryActivatingLean4Features(
                     elanCommandProvider,
                     resolve,
                     d,
-                    projectUri,
+                    info.projectRootUri,
                 )
                 return 'Stop'
             }),

vscode-lean4/src/leanclient.ts

@@ -43,7 +43,6 @@ import {
 } from './config'
 import { logger } from './utils/logger'
 // @ts-ignore
-import path from 'path'
 import { SemVer } from 'semver'
 import {
     c2pConverter,
@@ -368,7 +367,7 @@ export class LeanClient implements Disposable {
             return
         }
 
-        const fileName = fileUri.scheme === 'file' ? path.basename(fileUri.fsPath) : 'untitled'
+        const fileName = fileUri.scheme === 'file' ? fileUri.baseName() : 'untitled'
         const isImportsOutdatedError = params.diagnostics.some(
             d =>
                 d.severity === DiagnosticSeverity.Error &&
@@ -472,7 +471,7 @@ export class LeanClient implements Disposable {
 
     async restartFile(leanDoc: LeanDocument): Promise<void> {
         const extUri = leanDoc.extUri
-        const formattedFileName = extUri.scheme === 'file' ? path.basename(extUri.fsPath) : extUri.toString()
+        const formattedFileName = extUri.scheme === 'file' ? extUri.baseName() : extUri.toString()
         const formattedProjectName =
             this.folderUri.scheme === 'file' ? this.folderUri.fsPath : this.folderUri.toString()
         if (this.client === undefined || !this.running) {
@@ -592,7 +591,7 @@ export class LeanClient implements Disposable {
             documentSelector.pattern = `${escapedPath}/**/*`
             workspaceFolder = {
                 uri: this.folderUri.asUri(),
-                name: path.basename(this.folderUri.fsPath),
+                name: this.folderUri.baseName(),
                 index: 0, // the language client library does not actually need this index
             }
         }

vscode-lean4/src/projectinit.ts

@@ -14,7 +14,6 @@ import { lake } from './utils/lake'
 import { LeanInstaller } from './utils/leanInstaller'
 import { displayNotification, displayNotificationWithInput } from './utils/notifs'
 import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo'
-import path from 'path'
 
 const projectInitNotificationOptions: SetupNotificationOptions = {
     errorMode: { mode: 'NonModal' },
@@ -192,7 +191,7 @@ export class ProjectInitializationProvider implements Disposable {
             return 'DidNotComplete'
         }
 
-        const projectName: string = path.basename(projectFolder.fsPath)
+        const projectName: string = projectFolder.baseName()
         const result: ExecutionResult = await lake({
             channel: this.channel,
             cwdUri: projectFolder,
@@ -431,7 +430,7 @@ Open this project instead?`
     }
 
     private static async openNewFolder(projectFolder: FileUri) {
-        const message = `Project initialized. Open new project folder '${path.basename(projectFolder.fsPath)}'?`
+        const message = `Project initialized. Open new project folder '${projectFolder.baseName()}'?`
         const input = 'Open project folder'
         const choice: string | undefined = await displayNotificationWithInput('Information', message, [input])
         if (choice === input) {

vscode-lean4/src/utils/clientProvider.ts

@@ -1,16 +1,15 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
-import path from 'path'
 import { Disposable, EventEmitter, OutputChannel, commands } from 'vscode'
 import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics'
 import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs'
 import { LeanClient } from '../leanclient'
 import { LeanPublishDiagnosticsParams } from './converters'
-import { ExtUri, FileUri, UntitledUri } from './exturi'
+import { ExtUri, FileUri } from './exturi'
 import { lean } from './leanEditorProvider'
 import { LeanInstaller } from './leanInstaller'
 import { logger } from './logger'
 import { displayNotification } from './notifs'
-import { findLeanProjectRoot, willUseLakeServer } from './projectInfo'
+import { findLeanProjectRootInfo, willUseLakeServer } from './projectInfo'
 
 async function checkLean4ProjectPreconditions(
     channel: OutputChannel,
@@ -113,11 +112,6 @@ export class LeanClientProvider implements Disposable {
                 break
             }
             try {
-                const projectUri = await findLeanProjectRoot(uri)
-                if (projectUri === 'FileNotFound') {
-                    continue
-                }
-
                 const [cached, client] = await this.ensureClient(uri)
                 if (cached && client) {
                     await client.restart()
@@ -130,7 +124,7 @@ export class LeanClientProvider implements Disposable {
     }
 
     restartFile(uri: ExtUri) {
-        const fileName = uri.scheme === 'file' ? path.basename(uri.fsPath) : 'untitled file'
+        const fileName = uri.scheme === 'file' ? uri.baseName() : 'untitled file'
 
         const client: LeanClient | undefined = this.findClient(uri)
         if (!client || !client.isRunning()) {
@@ -243,10 +237,18 @@ export class LeanClientProvider implements Disposable {
     }
 
     async ensureClient(uri: ExtUri): Promise<[boolean, LeanClient | undefined]> {
-        const folderUri = uri.scheme === 'file' ? await findLeanProjectRoot(uri) : new UntitledUri()
-        if (folderUri === 'FileNotFound') {
+        const projectInfo = await findLeanProjectRootInfo(uri)
+        if (projectInfo.kind === 'FileNotFound') {
+            return [false, undefined]
+        }
+        if (projectInfo.kind === 'LakefileWithoutToolchain') {
+            displayNotification(
+                'Error',
+                `Project at ${projectInfo.projectRootUri} has a Lakefile, but lacks a 'lean-toolchain' file. Please create one with the Lean version that you would like the project to use.`,
+            )
             return [false, undefined]
         }
+        const folderUri = projectInfo.projectRootUri
         let client = this.getClientForFolder(folderUri)
         if (client) {
             this.activeClient = client

vscode-lean4/src/utils/configwatchservice.ts

@@ -1,7 +1,7 @@
 import * as path from 'path'
 import { Disposable, EventEmitter, Uri, window, workspace } from 'vscode'
 import { FileUri } from './exturi'
-import { findLeanProjectInfo, findLeanProjectRoot } from './projectInfo'
+import { findLeanProjectInfo, findLeanProjectRootInfo } from './projectInfo'
 
 // This service monitors the Lean package root folders for changes to any
 // lean-toolchail, lakefile.lean or lakefile.toml files found there.
@@ -78,8 +78,12 @@ export class LeanConfigWatchService implements Disposable {
         // Note: just opening the file fires this event sometimes which is annoying, so
         // we compare the contents just to be sure and normalize whitespace so that
         // just adding a new line doesn't trigger the prompt.
-        const projectUri = await findLeanProjectRoot(fileUri)
-        if (projectUri === 'FileNotFound') {
+        const info = await findLeanProjectRootInfo(fileUri)
+        if (
+            info.kind === 'FileNotFound' ||
+            info.kind === 'LakefileWithoutToolchain' ||
+            info.projectRootUri.scheme === 'untitled'
+        ) {
             return
         }
 
@@ -96,7 +100,7 @@ export class LeanConfigWatchService implements Disposable {
         this.normalizedLakeFileContents.set(key, contents)
         if (raiseEvent) {
             // raise an event so the extension triggers handleLakeFileChanged.
-            this.lakeFileChangedEmitter.fire(projectUri)
+            this.lakeFileChangedEmitter.fire(info.projectRootUri)
         }
     }
 
@@ -111,6 +115,8 @@ export class LeanConfigWatchService implements Disposable {
         const projectInfo = await findLeanProjectInfo(fileUri)
         if (
             projectInfo.kind === 'FileNotFound' ||
+            projectInfo.kind === 'LakefileWithoutToolchain' ||
+            projectInfo.projectRootUri.scheme === 'untitled' ||
             projectInfo.toolchainInfo === undefined ||
             projectInfo.toolchainInfo.toolchain === undefined
         ) {

vscode-lean4/src/utils/exturi.ts

@@ -1,3 +1,4 @@
+import path from 'path'
 import { Uri, workspace } from 'vscode'
 import { isFileInFolder, relativeFilePathInFolder } from './fsHelper'
 
@@ -49,6 +50,10 @@ export class FileUri {
         return this.asUri().toString()
     }
 
+    baseName(): string {
+        return path.basename(this.fsPath)
+    }
+
     join(...pathSegments: string[]): FileUri {
         return FileUri.fromUriOrError(Uri.joinPath(this.asUri(), ...pathSegments))
     }

vscode-lean4/src/utils/lake.ts

@@ -1,4 +1,3 @@
-import path from 'path'
 import { OutputChannel } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from './batch'
 import { FileUri } from './exturi'
@@ -50,7 +49,7 @@ export class LakeRunner {
     }
 
     async fetchMathlibCacheForFile(projectRelativeFileUri: FileUri): Promise<ExecutionResult> {
-        const prompt = `Fetching Mathlib build artifact cache for ${path.basename(projectRelativeFileUri.fsPath)}`
+        const prompt = `Fetching Mathlib build artifact cache for ${projectRelativeFileUri.baseName()}`
         return this.runLakeCommandWithProgress('exe', ['cache', 'get', projectRelativeFileUri.fsPath], prompt)
     }
 

vscode-lean4/src/utils/leanCmdRunner.ts

@@ -43,7 +43,7 @@ function overrideReason(activeOverride: ElanOverrideReason | undefined): string
         case 'Environment':
             return undefined
         case 'Manual':
-            return `set by \`elan override\` in folder '${path.basename(activeOverride.directoryPath.fsPath)}'`
+            return `set by \`elan override\` in folder '${activeOverride.directoryPath.baseName()}'`
         case 'ToolchainFile':
             return `of Lean project '${path.dirname(activeOverride.toolchainPath.fsPath)}'`
         case 'LeanpkgFile':