diff --git a/.vscode/launch.json b/.vscode/launch.json index 854e75c2b..b5b74cf0f 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -17,24 +17,6 @@ "webRoot": "${workspaceRoot}/vscode-lean4/media" } }, - { - "name": "Extension Tests - pre-bootstrap tests", - "type": "extensionHost", - "request": "launch", - "runtimeExecutable": "${execPath}", - "args": [ - "--extensionDevelopmentPath=${workspaceFolder}/vscode-lean4", - "--extensionTestsPath=${workspaceFolder}/vscode-lean4/out/test/suite/index", - "${workspaceFolder}/vscode-lean4/test/test-fixtures/simple" - ], - "env": { - "LEAN4_TEST_FOLDER": "pre-bootstrap", - "LEAN4_PROMPT_USER": "true" - }, - "cwd": "${workspaceFolder}/vscode-lean4/out/", - "outFiles": ["${workspaceFolder}/vscode-lean4/out/test/suite/**/*.js"], - "preLaunchTask": "watchTest" - }, { "name": "Extension Tests - bootstrap tests", "type": "extensionHost", @@ -67,23 +49,6 @@ "outFiles": ["${workspaceFolder}/vscode-lean4/out/test/suite/**/*.js"], "preLaunchTask": "watchTest" }, - { - "name": "Extension Tests - adhoc with no elan", - "type": "extensionHost", - "request": "launch", - "runtimeExecutable": "${execPath}", - "args": [ - "--extensionDevelopmentPath=${workspaceFolder}/vscode-lean4", - "--extensionTestsPath=${workspaceFolder}/vscode-lean4/out/test/suite/index" - ], - "env": { - "LEAN4_TEST_FOLDER": "simple", - "DISABLE_ELAN": "1" - }, - "cwd": "${workspaceFolder}/vscode-lean4/out/", - "outFiles": ["${workspaceFolder}/vscode-lean4/out/test/suite/**/*.js"], - "preLaunchTask": "watchTest" - }, { "name": "Extension Tests - infoview", "type": "extensionHost", diff --git a/README.md b/README.md index aaaa148d9..d5ff15bff 100644 --- a/README.md +++ b/README.md @@ -157,14 +157,6 @@ This extension contributes the following settings (for a complete list, open the ### Server settings -* `lean4.toolchainPath`: specifies the location of the Lean toolchain to be used when starting the Lean language server. Most users (i.e. those using `elan`) should not ever need to change this. If you are bundling Lean and `vscode-lean` with [Portable mode VS Code](https://code.visualstudio.com/docs/editor/portable), you might find it useful to specify a relative path to Lean. This can be done by starting this setting string with `%extensionPath%`; the extension will replace this with the absolute path of the extension folder. For example, with the default directory setup in Portable mode, `%extensionPath%/../../../lean` will point to `lean` in the same folder as the VS Code executable / application. - -* `lean4.lakePath`: specifies the location of the Lake executable to be used when starting the Lean language server (when possible). If left unspecified, the extension defaults to the Lake executable bundled with the Lean toolchain. Most users thus do not need to use this setting. It is only really helpful if you are building a Lake executable from the source and wish to use it with this extension. - -* `lean4.serverEnv`: specifies any Environment variables to add to the Lean 4 language server environment. Note that when opening a [remote folder](https://code.visualstudio.com/docs/remote/ssh) using VS Code the Lean 4 language server will be running on that remote machine. - -* `lean4.serverEnvPaths`: specifies any additional paths to add to the Lean 4 language server environment PATH variable. - * `lean4.serverArgs`: specifies any additional arguments to pass on the `lean --server` command line. * `lean4.serverLogging.enabled`: specifies whether to do additional logging of diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json index 92fb2ce56..87984dd7a 100644 --- a/lean4-infoview-api/package.json +++ b/lean4-infoview-api/package.json @@ -14,7 +14,7 @@ ], "license": "Apache-2.0", "devDependencies": { - "typescript": "^4.9.5", + "typescript": "^5.4.5", "vscode-languageserver-protocol": "^3.17.3" } } diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json index 0254410e4..55b9fb958 100644 --- a/lean4-infoview/package.json +++ b/lean4-infoview/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview", - "version": "0.6.1", + "version": "0.7.0", "description": "An interactive display for the Lean 4 theorem prover.", "scripts": { "watch": "rollup --config --environment NODE_ENV:development --watch", @@ -39,12 +39,12 @@ "@types/marked": "^4.3.1", "@types/react": "^18.2.15", "@types/react-dom": "^18.2.7", - "current-release": "npm:@leanprover/infoview@^0.4.0", + "current-release": "npm:@leanprover/infoview@^0.7.0", "react": "^18.2.0", "react-dom": "^18.2.0", "rollup": "^3.26.2", "rollup-plugin-css-only": "^4.3.0", - "typescript": "^4.9.5" + "typescript": "^5.4.5" }, "dependencies": { "@leanprover/infoview-api": "~0.4.0", diff --git a/package-lock.json b/package-lock.json index a61173b8f..9c9586ef1 100644 --- a/package-lock.json +++ b/package-lock.json @@ -21,12 +21,12 @@ "lint-staged": "^15.2.2", "prettier": "3.2.5", "prettier-plugin-organize-imports": "^3.2.4", - "typescript": "^4.9.5" + "typescript": "^5.4.5" } }, "lean4-infoview": { "name": "@leanprover/infoview", - "version": "0.6.1", + "version": "0.7.0", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview-api": "~0.4.0", @@ -49,12 +49,12 @@ "@types/marked": "^4.3.1", "@types/react": "^18.2.15", "@types/react-dom": "^18.2.7", - "current-release": "npm:@leanprover/infoview@^0.4.0", + "current-release": "npm:@leanprover/infoview@^0.7.0", "react": "^18.2.0", "react-dom": "^18.2.0", "rollup": "^3.26.2", "rollup-plugin-css-only": "^4.3.0", - "typescript": "^4.9.5" + "typescript": "^5.4.5" } }, "lean4-infoview-api": { @@ -62,7 +62,7 @@ "version": "0.4.0", "license": "Apache-2.0", "devDependencies": { - "typescript": "^4.9.5", + "typescript": "^5.4.5", "vscode-languageserver-protocol": "^3.17.3" } }, @@ -4262,18 +4262,19 @@ }, "node_modules/current-release": { "name": "@leanprover/infoview", - "version": "0.4.5", - "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.5.tgz", - "integrity": "sha512-CK1Etux2e9lBg/eiDb0laj5Y9VAcPquLd9wdWU/GOiL1XAT64MVsGvhUsHr+LbZq6bxQn8JIgSfKgnHGTKwigg==", + "version": "0.7.0", + "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.7.0.tgz", + "integrity": "sha512-6Ke8MWU/EyGOX/vBguhK7zCtmCILWkYtr15qmS6JvR8AvIl2z9Dj2NhwsAVAv42ia326RRU09IWvx7uwT5Ahqw==", "dev": true, "dependencies": { - "@leanprover/infoview-api": "~0.2.1", + "@leanprover/infoview-api": "~0.4.0", "@vscode/codicons": "^0.0.32", - "es-module-shims": "^1.6.2", - "marked": "^4.2.2", - "react-fast-compare": "^3.2.0", + "@vscode/webview-ui-toolkit": "^1.4.0", + "es-module-shims": "^1.7.3", + "marked": "^4.3.0", + "react-fast-compare": "^3.2.2", "tachyons": "^4.12.0", - "vscode-languageserver-protocol": "^3.17.2" + "vscode-languageserver-protocol": "^3.17.3" } }, "node_modules/dargs": { @@ -12667,16 +12668,16 @@ "dev": true }, "node_modules/typescript": { - "version": "4.9.5", - "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.5.tgz", - "integrity": "sha512-1FXk9E2Hm+QzZQ7z+McJiHL4NW1F2EzMu9Nq9i3zAaGqibafqYwCVU6WyWAuyQRRzOlxou8xZSyXLEN8oKj24g==", + "version": "5.4.5", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.4.5.tgz", + "integrity": "sha512-vcI4UpRgg81oIRUFwR0WSIHKt11nJ7SAVlYNIu+QpqeyXP+gpQJy/Z4+F0aGxSE4MqwjyXvW/TzgkLAx2AGHwQ==", "dev": true, "bin": { "tsc": "bin/tsc", "tsserver": "bin/tsserver" }, "engines": { - "node": ">=4.2.0" + "node": ">=14.17" } }, "node_modules/uc.micro": { @@ -13439,10 +13440,10 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.142", + "version": "0.0.143", "license": "Apache-2.0", "dependencies": { - "@leanprover/infoview": "~0.6.1", + "@leanprover/infoview": "~0.7.0", "@leanprover/infoview-api": "~0.4.0", "axios": "^1.6.7", "cheerio": "^1.0.0-rc.12", @@ -13468,7 +13469,7 @@ "ovsx": "^0.8.3", "source-map-loader": "^3.0.2", "ts-loader": "^9.5.1", - "typescript": "^4.9.5", + "typescript": "^5.4.5", "webpack": "^5.90.3", "webpack-cli": "^4.10.0" }, diff --git a/package.json b/package.json index 4214b4159..e05270a40 100644 --- a/package.json +++ b/package.json @@ -25,7 +25,7 @@ "lint-staged": "^15.2.2", "prettier": "3.2.5", "prettier-plugin-organize-imports": "^3.2.4", - "typescript": "^4.9.5" + "typescript": "^5.4.5" }, "lint-staged": { "*.{ts,tsx,js}": [ diff --git a/vscode-lean4/media/guide-help.md b/vscode-lean4/media/guide-help.md index 0f0c7472c..6622fc21b 100644 --- a/vscode-lean4/media/guide-help.md +++ b/vscode-lean4/media/guide-help.md @@ -1,9 +1,11 @@ ## Collecting VS Code Output -If you are encountering an issue with this VS Code extension, copying the output from the 'Lean: Editor' output panel can be helpful for others who are trying to help you. +If you are encountering an issue with Lean or this VS Code extension, copying the output from the 'Lean: Editor' output panel can be helpful for others who are trying to help you. You can open the 'Lean: Editor' output panel by clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Output'. ![Show Output](show-output.png) +Additionally, copying the information that is displayed when clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Setup Information' is also very helpful. + ## Asking Questions on the Lean Zulip Chat To post a question on the [Lean Zulip chat](https://leanprover.zulipchat.com/), you can follow these steps: diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 683ce5671..24b5dc2b4 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -22,12 +22,6 @@ "type": "object", "title": "Lean 4", "properties": { - "lean4.toolchainPath": { - "type": "string", - "default": "", - "markdownDescription": "**DO NOT CHANGE** unless you know what you are doing. Path to your Lean toolchain. Leave this blank to get the default location from your PATH environment or from the default elan install location.", - "scope": "machine-overridable" - }, "lean4.input.enabled": { "type": "boolean", "default": true, @@ -73,36 +67,14 @@ "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.serverEnv": { - "type": "object", - "default": {}, - "description": "Environment variables to add to the Lean 4 server environment", - "additionalProperties": { - "type": "string", - "description": "environment variable to add" - }, - "scope": "machine-overridable" - }, - "lean4.serverEnvPaths": { + "lean4.envPathExtensions": { "type": "array", "default": [], - "description": "Paths to add to the Lean 4 server environment PATH variable.", + "markdownDescription": "Additional entries to add to the PATH variable of the Lean 4 VS Code extension process and any of its child processes.", "items": { "type": "string", - "description": "a path to add to the environment" - }, - "scope": "machine-overridable" - }, - "lean4.enableLake": { - "type": "boolean", - "default": true, - "markdownDescription": "Enable Lake server when possible." - }, - "lean4.lakePath": { - "type": "string", - "default": "", - "markdownDescription": "Path to Lake. Leave this blank to use the Lake from the toolchain.", - "scope": "machine-overridable" + "description": "Entry to add to the PATH variable" + } }, "lean4.serverArgs": { "type": "array", @@ -184,10 +156,10 @@ "default": 200, "description": "Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower values may make editing feel faster at the cost of higher CPU usage." }, - "lean4.showInvalidProjectWarnings": { + "lean4.showSetupWarnings": { "type": "boolean", "default": true, - "markdownDescription": "Show warnings whenever a .lean-file is opened in a folder that does not contain a 'lean-toolchain' file." + "markdownDescription": "Show warning notifications when the Lean setup has warning-level issues." }, "lean4.alwaysShowTitleBarMenu": { "type": "boolean", @@ -313,6 +285,12 @@ "title": "Troubleshooting: Show Output", "description": "Show output channel containing all progress updates and errors of commands" }, + { + "command": "lean4.troubleshooting.showSetupInformation", + "category": "Lean 4", + "title": "Troubleshooting: Show Setup Information", + "description": "Show setup information for the environment that the VS Code extension is running in" + }, { "command": "lean4.setup.showSetupGuide", "category": "Lean 4", @@ -561,6 +539,9 @@ { "command": "lean4.troubleshooting.showOutput" }, + { + "command": "lean4.troubleshooting.showSetupInformation" + }, { "command": "lean4.setup.showSetupGuide" }, @@ -634,6 +615,11 @@ "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", "group": "4_troubleshooting" }, + { + "command": "lean4.troubleshooting.showSetupInformation", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "4_troubleshooting" + }, { "submenu": "lean4.titlebar.versions", "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", @@ -902,7 +888,7 @@ "test": "node ./out/test/suite/runTest.js" }, "dependencies": { - "@leanprover/infoview": "~0.6.1", + "@leanprover/infoview": "~0.7.0", "@leanprover/infoview-api": "~0.4.0", "axios": "^1.6.7", "cheerio": "^1.0.0-rc.12", @@ -928,7 +914,7 @@ "ovsx": "^0.8.3", "source-map-loader": "^3.0.2", "ts-loader": "^9.5.1", - "typescript": "^4.9.5", + "typescript": "^5.4.5", "webpack": "^5.90.3", "webpack-cli": "^4.10.0" }, diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index 339122615..94a71a2a4 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -1,157 +1,20 @@ -import * as fs from 'fs' -import * as path from 'path' import { workspace } from 'vscode' -import { logger } from './utils/logger' +import { PATH } from './utils/envPath' // TODO: does currently not contain config options for `./abbreviation` // so that it is easy to keep it in sync with vscode-lean. -export function getEnvPath(): string { - if (process.platform === 'win32') { - return process.env.Path ?? '' - } else { - return process.env.PATH ?? '' - } -} - -export function setEnvPath(value: string): void { - if (process.platform === 'win32') { - process.env.Path = value - } else { - process.env.PATH = value - } -} - -function splitEnvPath(value: string): string[] { - return value.split(path.delimiter) -} - -function joinEnvPath(value: string[]): string { - return value.join(path.delimiter) -} - -// Make a copy of the passed process environment that includes the user's -// `lean4.serverEnvPaths` in the path key, and adds the key/value pairs from -// `lean4.serverEnv`. Both of these settings can be found in the user's -// settings.json file -export function addServerEnvPaths(input_env: NodeJS.ProcessEnv): NodeJS.ProcessEnv { - const env = Object.assign({}, input_env, serverEnv()) - const paths = serverEnvPaths() - if (paths.length !== 0) { - setEnvPath(joinEnvPath(paths) + path.delimiter + getEnvPath()) - } - return env -} - -export function getDefaultElanPath(): string { - let elanPath = '' - if (process.platform === 'win32') { - elanPath = process.env.USERPROFILE + '\\.elan\\bin' - } else { - elanPath = process.env.HOME + '/.elan/bin' - } - return elanPath -} - -export function addDefaultElanPath(): void { - const paths = getEnvPath() - const elanPath = getDefaultElanPath() - if (paths.indexOf(elanPath) < 0) { - setEnvPath(paths + path.delimiter + elanPath) - } -} - -function findToolchainBin(root: string): string { - logger.log(`Looking for toolchains in ${root}`) - if (!fs.existsSync(root)) { - return '' - } - const toolchains = fs.readdirSync(path.join(root, '..', 'toolchains')) - for (const toolchain of toolchains) { - if (toolchain.indexOf('leanprover--lean4') >= 0) { - return path.join(root, '..', 'toolchains', toolchains[0], 'bin') - } - } - return '' -} - -export function addToolchainBinPath(elanPath: string) { - const bin = findToolchainBin(elanPath) - if (bin) { - const paths = getEnvPath() - setEnvPath(paths + path.delimiter + bin) - } -} - -export function findProgramInPath(name: string): string { - if (fs.existsSync(name)) { - return name - } - const extensions: string[] = [] - if (process.platform === 'win32') { - extensions.push('.exe') - extensions.push('.com') - extensions.push('.cmd') - } else { - extensions.push('') - } - const parts = splitEnvPath(getEnvPath()) - for (const part of parts) { - for (const ext of extensions) { - const fullPath = path.join(part, name + ext) - if (fs.existsSync(fullPath)) { - return fullPath - } - } - } - return '' -} - -export function removeElanPath(): string { - const parts = splitEnvPath(getEnvPath()) - let result = '' - for (let i = 0; i < parts.length; ) { - const part = parts[i] - if (part.indexOf('.elan') > 0) { - logger.log(`removing path to elan: ${part}`) - result = part - parts.splice(i, 1) - } else { - i++ - } - } - - setEnvPath(joinEnvPath(parts)) - return result -} - export function getPowerShellPath(): string { const windir = process.env.windir return `${windir}\\System32\\WindowsPowerShell\\v1.0\\powershell.exe` } -export function toolchainPath(): string { - return workspace.getConfiguration('lean4').get('toolchainPath', '') -} - -export function lakePath(): string { - return workspace.getConfiguration('lean4').get('lakePath', '') -} - -export function lakeEnabled(): boolean { - return workspace.getConfiguration('lean4').get('enableLake', false) -} - -export function serverEnv(): object { - return workspace.getConfiguration('lean4').get('serverEnv', {}) -} - export function automaticallyBuildDependencies(): boolean { return workspace.getConfiguration('lean4').get('automaticallyBuildDependencies', false) } -export function serverEnvPaths(): string[] { - return workspace.getConfiguration('lean4').get('serverEnvPaths', []) +export function envPathExtensions(): PATH { + return new PATH(workspace.getConfiguration('lean4').get('envPathExtensions', [])) } export function serverArgs(): string[] { @@ -223,21 +86,14 @@ export function getElaborationDelay(): number { return workspace.getConfiguration('lean4').get('elaborationDelay', 200) } -export function shouldShowInvalidProjectWarnings(): boolean { - return workspace.getConfiguration('lean4').get('showInvalidProjectWarnings', true) +export function shouldShowSetupWarnings(): boolean { + return workspace.getConfiguration('lean4').get('showSetupWarnings', true) } export function getFallBackToStringOccurrenceHighlighting(): boolean { return workspace.getConfiguration('lean4').get('fallBackToStringOccurrenceHighlighting', false) } -export function getLeanExecutableName(): string { - if (process.platform === 'win32') { - return 'lean.exe' - } - return 'lean' -} - export function isRunningTest(): boolean { return typeof process.env.LEAN4_TEST_FOLDER === 'string' } @@ -252,10 +108,6 @@ export function getDefaultLeanVersion(): string { : 'leanprover/lean4:stable' } -export function isElanDisabled(): boolean { - return typeof process.env.DISABLE_ELAN === 'string' -} - /** The editor line height, in pixels. */ export function getEditorLineHeight(): number { // The implementation diff --git a/vscode-lean4/src/exports.ts b/vscode-lean4/src/exports.ts index 2a50c8905..6cfc9179f 100644 --- a/vscode-lean4/src/exports.ts +++ b/vscode-lean4/src/exports.ts @@ -1,17 +1,39 @@ +import { OutputChannel } from 'vscode' import { DocViewProvider } from './docview' import { InfoProvider } from './infoview' import { ProjectInitializationProvider } from './projectinit' import { ProjectOperationProvider } from './projectoperations' import { LeanClientProvider } from './utils/clientProvider' import { LeanInstaller } from './utils/leanInstaller' +import { FullDiagnosticsProvider } from './utils/setupDiagnostics' -export interface Exports { - isLean4Project: boolean - version: string | undefined - infoProvider: InfoProvider | undefined - clientProvider: LeanClientProvider | undefined - projectOperationProvider: ProjectOperationProvider | undefined - installer: LeanInstaller | undefined - docView: DocViewProvider | undefined - projectInitializationProver: ProjectInitializationProvider | undefined +export interface AlwaysEnabledFeatures { + docView: DocViewProvider + projectInitializationProvider: ProjectInitializationProvider + outputChannel: OutputChannel + installer: LeanInstaller + fullDiagnosticsProvider: FullDiagnosticsProvider +} + +export interface Lean4EnabledFeatures { + clientProvider: LeanClientProvider + infoProvider: InfoProvider + projectOperationProvider: ProjectOperationProvider +} + +export interface EnabledFeatures extends AlwaysEnabledFeatures, Lean4EnabledFeatures {} + +export class Exports { + alwaysEnabledFeatures: AlwaysEnabledFeatures + lean4EnabledFeatures: Promise + + constructor(alwaysEnabledFeatures: AlwaysEnabledFeatures, lean4EnabledFeatures: Promise) { + this.alwaysEnabledFeatures = alwaysEnabledFeatures + this.lean4EnabledFeatures = lean4EnabledFeatures + } + + async allFeatures(): Promise { + const lean4EnabledFeatures = await this.lean4EnabledFeatures + return { ...this.alwaysEnabledFeatures, ...lean4EnabledFeatures } + } } diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 9da2d1ba2..614368600 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -1,15 +1,11 @@ +import * as os from 'os' +import * as path from 'path' import { commands, Disposable, ExtensionContext, extensions, TextDocument, window, workspace } from 'vscode' import { AbbreviationFeature } from './abbreviation' -import { - addDefaultElanPath, - addToolchainBinPath, - getDefaultElanPath, - getDefaultLeanVersion, - isElanDisabled, - removeElanPath, -} from './config' +import { getDefaultLeanVersion } from './config' import { DocViewProvider } from './docview' -import { Exports } from './exports' +import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports' +import { checkLean4FeaturePreconditions } from './globalDiagnostics' import { InfoProvider } from './infoview' import { LeanClient } from './leanclient' import { ProjectInitializationProvider } from './projectinit' @@ -17,22 +13,13 @@ import { ProjectOperationProvider } from './projectoperations' import { LeanTaskGutter } from './taskgutter' import { LeanClientProvider } from './utils/clientProvider' import { LeanConfigWatchService } from './utils/configwatchservice' -import { isExtUri, toExtUriOrError, UntitledUri } from './utils/exturi' +import { PATH, setProcessEnvPATH } from './utils/envPath' +import { isExtUri, toExtUriOrError } from './utils/exturi' import { LeanInstaller } from './utils/leanInstaller' -import { logger } from './utils/logger' -import { findLeanPackageVersionInfo } from './utils/projectInfo' - -interface AlwaysEnabledFeatures { - docView: DocViewProvider - projectInitializationProvider: ProjectInitializationProvider - installer: LeanInstaller -} - -interface Lean4EnabledFeatures { - clientProvider: LeanClientProvider - infoProvider: InfoProvider - projectOperationProvider: ProjectOperationProvider -} +import { displayWarning } from './utils/notifs' +import { PathExtensionProvider } from './utils/pathExtensionProvider' +import { findLeanProjectRoot } from './utils/projectInfo' +import { FullDiagnosticsProvider, PreconditionCheckResult } from './utils/setupDiagnostics' async function setLeanFeatureSetActive(isActive: boolean) { await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive) @@ -59,19 +46,24 @@ function findOpenLeanDocument(): TextDocument | undefined { return undefined } +function getElanPath(): string { + return path.join(os.homedir(), '.elan', 'bin') +} + +function addElanPathToPATH() { + const path = PATH.ofProcessEnv() + const elanPath = getElanPath() + if (!path.includes(elanPath)) { + setProcessEnvPATH(path.prepend(elanPath)) + } +} + /** * Activates all extension features that are *always* enabled, even when no Lean 4 document is currently open. */ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabledFeatures { - // For unit test that tests behavior when there is no elan installed. - if (isElanDisabled()) { - const elanRoot = removeElanPath() - if (elanRoot) { - addToolchainBinPath(elanRoot) - } - } else { - addDefaultElanPath() - } + addElanPathToPATH() + context.subscriptions.push(PathExtensionProvider.withAddedEnvPathExtensions()) context.subscriptions.push( commands.registerCommand('lean4.setup.showSetupGuide', async () => @@ -93,21 +85,12 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled const installer = new LeanInstaller(outputChannel, defaultToolchain) - context.subscriptions.push( - commands.registerCommand('lean4.setup.installElan', async () => { - await installer.installElan() - if (isElanDisabled()) { - addToolchainBinPath(getDefaultElanPath()) - } else { - addDefaultElanPath() - } - }), - ) + context.subscriptions.push(commands.registerCommand('lean4.setup.installElan', () => installer.installElan())) const checkForExtensionConflict = (doc: TextDocument) => { const isLean3ExtensionInstalled = extensions.getExtension('jroesch.lean') !== undefined if (isLean3ExtensionInstalled && (doc.languageId === 'lean' || doc.languageId === 'lean4')) { - void window.showWarningMessage( + displayWarning( "The Lean 3 and the Lean 4 VS Code extension are enabled at the same time. Since both extensions act on .lean files, this can lead to issues with either extension. Please disable the extension for the Lean major version that you do not want to use ('Extensions' in the left sidebar > Cog icon > 'Disable').", ) } @@ -117,34 +100,10 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled } context.subscriptions.push(workspace.onDidOpenTextDocument(checkForExtensionConflict)) - return { docView, projectInitializationProvider, installer } -} - -async function isLean3Project(installer: LeanInstaller): Promise { - const doc = findOpenLeanDocument() - if (!doc) { - const versionInfo = await installer.checkLeanVersion(new UntitledUri(), installer.getDefaultToolchain()) - return versionInfo.version === '3' - } - - const docUri = toExtUriOrError(doc.uri) - const [packageUri, toolchainVersion] = - docUri.scheme === 'file' ? await findLeanPackageVersionInfo(docUri) : [new UntitledUri(), undefined] - - if (toolchainVersion && toolchainVersion.indexOf('lean:3') > 0) { - logger.log(`Lean4 skipping lean 3 project: ${toolchainVersion}`) - return true - } - - const versionInfo = await installer.checkLeanVersion( - packageUri, - toolchainVersion ?? installer.getDefaultToolchain(), - ) - if (versionInfo.version === '3') { - return true - } + const fullDiagnosticsProvider = new FullDiagnosticsProvider(outputChannel) + context.subscriptions.push(fullDiagnosticsProvider) - return false + return { docView, projectInitializationProvider, outputChannel, installer, fullDiagnosticsProvider } } function activateAbbreviationFeature(context: ExtensionContext, docView: DocViewProvider): AbbreviationFeature { @@ -158,12 +117,20 @@ function activateAbbreviationFeature(context: ExtensionContext, docView: DocView async function activateLean4Features( context: ExtensionContext, installer: LeanInstaller, -): Promise { + doc: TextDocument, +): Promise { + const docUri = toExtUriOrError(doc.uri) + const cwd = docUri.scheme === 'file' ? await findLeanProjectRoot(docUri) : undefined + const preconditionCheckResult = await checkLean4FeaturePreconditions(installer, cwd) + if (preconditionCheckResult === PreconditionCheckResult.Fatal) { + return undefined + } + const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel()) context.subscriptions.push(clientProvider) const watchService = new LeanConfigWatchService() - watchService.versionChanged(async packageUri => { + watchService.versionChanged(packageUri => { const client: LeanClient | undefined = clientProvider.getClientForFolder(packageUri) if (client && !client.isRunning()) { // This can naturally happen when we update the Lean version using the "Update Dependency" command @@ -171,7 +138,7 @@ async function activateLean4Features( // message in this case. return } - await installer.handleVersionChanged(packageUri) + installer.handleVersionChanged(packageUri) }) watchService.lakeFileChanged(packageUri => installer.handleLakeFileChanged(packageUri)) context.subscriptions.push(watchService) @@ -191,69 +158,42 @@ async function activateLean4Features( return { clientProvider, infoProvider, projectOperationProvider } } -let extensionExports: Exports - export async function activate(context: ExtensionContext): Promise { await setLeanFeatureSetActive(false) const alwaysEnabledFeatures: AlwaysEnabledFeatures = activateAlwaysEnabledFeatures(context) - - if (await isLean3Project(alwaysEnabledFeatures.installer)) { - extensionExports = { - isLean4Project: false, - version: '3', - infoProvider: undefined, - clientProvider: undefined, - projectOperationProvider: undefined, - installer: alwaysEnabledFeatures.installer, - docView: alwaysEnabledFeatures.docView, - projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider, - } - return extensionExports - } - activateAbbreviationFeature(context, alwaysEnabledFeatures.docView) - if (findOpenLeanDocument()) { - const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features( - context, - alwaysEnabledFeatures.installer, - ) - extensionExports = { - isLean4Project: true, - version: '4', - infoProvider: lean4EnabledFeatures.infoProvider, - clientProvider: lean4EnabledFeatures.clientProvider, - projectOperationProvider: lean4EnabledFeatures.projectOperationProvider, - installer: alwaysEnabledFeatures.installer, - docView: alwaysEnabledFeatures.docView, - projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider, + const lean4EnabledFeatures: Promise = new Promise(async (resolve, _) => { + const doc: TextDocument | undefined = findOpenLeanDocument() + if (doc) { + const lean4EnabledFeatures: Lean4EnabledFeatures | undefined = await activateLean4Features( + context, + alwaysEnabledFeatures.installer, + doc, + ) + if (lean4EnabledFeatures) { + resolve(lean4EnabledFeatures) + return + } } - return extensionExports - } - // No Lean 4 document yet => Load remaining features when one is open - const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => { - if (isLean4Document(doc)) { - const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features( + // No Lean 4 document yet => Load remaining features when one is open + const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => { + if (!isLean4Document(doc)) { + return + } + const lean4EnabledFeatures: Lean4EnabledFeatures | undefined = await activateLean4Features( context, alwaysEnabledFeatures.installer, + doc, ) - extensionExports.infoProvider = lean4EnabledFeatures.infoProvider - extensionExports.clientProvider = lean4EnabledFeatures.clientProvider - extensionExports.projectOperationProvider = lean4EnabledFeatures.projectOperationProvider + if (!lean4EnabledFeatures) { + return + } + resolve(lean4EnabledFeatures) disposeActivationListener.dispose() - } - }, context.subscriptions) + }, context.subscriptions) + }) - extensionExports = { - isLean4Project: true, - version: '4', - infoProvider: undefined, - clientProvider: undefined, - projectOperationProvider: undefined, - installer: alwaysEnabledFeatures.installer, - docView: alwaysEnabledFeatures.docView, - projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider, - } - return extensionExports + return new Exports(alwaysEnabledFeatures, lean4EnabledFeatures) } diff --git a/vscode-lean4/src/globalDiagnostics.ts b/vscode-lean4/src/globalDiagnostics.ts new file mode 100644 index 000000000..afc280b37 --- /dev/null +++ b/vscode-lean4/src/globalDiagnostics.ts @@ -0,0 +1,157 @@ +import { OutputChannel } from 'vscode' +import { ExecutionExitCode, displayResultError } from './utils/batch' +import { elanSelfUpdate } from './utils/elan' +import { FileUri } from './utils/exturi' +import { LeanInstaller } from './utils/leanInstaller' +import { + PreconditionCheckResult, + SetupDiagnoser, + diagnose, + displaySetupErrorWithInput, + displaySetupErrorWithOutput, + displaySetupErrorWithSetupGuide, + displaySetupWarningWithInput, + displaySetupWarningWithOutput, +} from './utils/setupDiagnostics' + +class GlobalDiagnosticsProvider { + readonly installer: LeanInstaller + readonly channel: OutputChannel + readonly cwdUri: FileUri | undefined + + constructor(installer: LeanInstaller, cwdUri: FileUri | undefined) { + this.installer = installer + this.channel = installer.getOutputChannel() + this.cwdUri = cwdUri + } + + private diagnose(): SetupDiagnoser { + return diagnose(this.channel, this.cwdUri) + } + + async checkDependenciesAreInstalled(): Promise { + const isCurlInstalled = await this.diagnose().checkCurlAvailable() + const isGitInstalled = await this.diagnose().checkGitAvailable() + if (isCurlInstalled && isGitInstalled) { + return true + } + + let missingDepMessage: string + if (!isCurlInstalled && isGitInstalled) { + missingDepMessage = "One of Lean's dependencies ('curl') is missing" + } else if (isCurlInstalled && !isGitInstalled) { + missingDepMessage = "One of Lean's dependencies ('git') is missing" + } else { + missingDepMessage = "Both of Lean's dependencies ('curl' and 'git') are missing" + } + + const errorMessage = `${missingDepMessage}. Please read the Setup Guide on how to install missing dependencies and set up Lean 4.` + displaySetupErrorWithSetupGuide(errorMessage) + return false + } + + async checkLean4IsInstalled(): Promise { + const leanVersionResult = await this.diagnose().queryLeanVersion() + switch (leanVersionResult.kind) { + case 'Success': + return true + + case 'CommandError': + displaySetupErrorWithOutput(`Error while checking Lean version: ${leanVersionResult.message}`) + return false + + case 'InvalidVersion': + displaySetupErrorWithOutput( + `Error while checking Lean version: 'lean --version' returned a version that could not be parsed: '${leanVersionResult.versionResult}'`, + ) + return false + + case 'CommandNotFound': + if (!this.installer.getPromptUser()) { + // Used in tests + await this.installer.autoInstall() + return true + } + + const installElanItem = 'Install Elan and Lean 4' + const installElanChoice = await displaySetupErrorWithInput( + "Lean is not installed. Do you want to install Lean's version manager Elan and a recent stable version of Lean 4?", + installElanItem, + ) + if (installElanChoice === undefined) { + return false + } + await this.installer.installElan() + return true + } + } + + async checkElanIsUpToDate(): Promise { + const elanDiagnosis = await this.diagnose().elanVersion() + + switch (elanDiagnosis.kind) { + case 'NotInstalled': + const installElanItem = 'Install Elan and Lean 4' + const installElanChoice = await displaySetupWarningWithInput( + "Lean's version manager Elan is not installed. This means that the correct Lean 4 toolchain version of Lean 4 projects will not be selected or installed automatically. Do you want to install Elan and a recent stable version of Lean 4?", + installElanItem, + ) + if (installElanChoice === undefined) { + return false + } + await this.installer.installElan() + return true + + case 'ExecutionError': + displaySetupWarningWithOutput('Cannot determine Elan version: ' + elanDiagnosis.message) + return false + + case 'Outdated': + const updateElanItem = 'Update Elan' + const updateElanChoice = await displaySetupWarningWithInput( + `Lean's version manager Elan is outdated: the installed version is ${elanDiagnosis.currentVersion.toString()}, but a version of ${elanDiagnosis.recommendedVersion.toString()} is recommended. Do you want to update Elan?`, + updateElanItem, + ) + if (updateElanChoice === undefined) { + return false + } + const elanSelfUpdateResult = await elanSelfUpdate(this.channel) + if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) { + displayResultError( + elanSelfUpdateResult, + "Cannot update Elan. If you suspect that this is due to the way that you have set up Elan (e.g. from a package repository that ships an outdated version of Elan), you can disable these warnings using the 'Lean4: Show Setup Warnings' setting under 'File' > 'Preferences' > 'Settings'.", + ) + return false + } + + return true + + case 'UpToDate': + return true + } + } +} + +export async function checkLean4FeaturePreconditions( + installer: LeanInstaller, + cwdUri: FileUri | undefined, +): Promise { + const diagnosticsProvider = new GlobalDiagnosticsProvider(installer, cwdUri) + + const areDependenciesInstalled = await diagnosticsProvider.checkDependenciesAreInstalled() + if (!areDependenciesInstalled) { + return PreconditionCheckResult.Fatal + } + + const isLean4Installed = await diagnosticsProvider.checkLean4IsInstalled() + if (!isLean4Installed) { + return PreconditionCheckResult.Fatal + } + + const isElanUpToDate = await diagnosticsProvider.checkElanIsUpToDate() + if (!isElanUpToDate) { + return PreconditionCheckResult.Warning + } + + return PreconditionCheckResult.Fulfilled +} diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 31349a408..80dd41862 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -52,6 +52,7 @@ import { LeanClientProvider } from './utils/clientProvider' import { c2pConverter, p2cConverter } from './utils/converters' import { ExtUri, parseExtUri, toExtUri } from './utils/exturi' import { logger } from './utils/logger' +import { displayError, displayInformation } from './utils/notifs' const keepAlivePeriodMs = 10000 @@ -257,7 +258,7 @@ export class InfoProvider implements Disposable { }, copyToClipboard: async text => { await env.clipboard.writeText(text) - await window.showInformationMessage(`Copied to clipboard: ${text}`) + displayInformation(`Copied to clipboard: ${text}`) }, insertText: async (text, kind, tdpp) => { let uri: ExtUri | undefined @@ -464,7 +465,7 @@ export class InfoProvider implements Disposable { this.workersFailed.set(uri, reason) } logger.log(`[InfoProvider]client crashed: ${uri}`) - await client.showRestartMessage(true, extUri) + client.showRestartMessage(true, extUri) } onClientRemoved(client: LeanClient) { @@ -488,7 +489,7 @@ export class InfoProvider implements Disposable { this.clientsFailed.set(key.toString(), reason) } logger.log(`[InfoProvider] client stopped: ${key}`) - await client.showRestartMessage() + client.showRestartMessage() } dispose(): void { @@ -585,7 +586,7 @@ export class InfoProvider implements Disposable { } else if (window.activeTextEditor && window.activeTextEditor.document.languageId === 'lean4') { await this.openPreview(window.activeTextEditor) } else { - void window.showErrorMessage( + displayError( 'No active Lean editor tab. Make sure to focus the Lean editor tab for which you want to open the infoview.', ) } diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index 72e551f03..b99629fa5 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -1,5 +1,4 @@ import { - ConfigurationChangeEvent, Diagnostic, DiagnosticCollection, Disposable, @@ -32,30 +31,28 @@ import { import * as ls from 'vscode-languageserver-protocol' import { LeanFileProgressParams, LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api' -import { join } from 'path' import { - addServerEnvPaths, automaticallyBuildDependencies, getElaborationDelay, getFallBackToStringOccurrenceHighlighting, - lakeEnabled, - lakePath, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput, - toolchainPath, } from './config' import { assert } from './utils/assert' -import { batchExecute, ExecutionExitCode, ExecutionResult } from './utils/batch' import { logger } from './utils/logger' -import { readLeanVersion } from './utils/projectInfo' // @ts-ignore import { SemVer } from 'semver' import { c2pConverter, p2cConverter, patchConverters } from './utils/converters' -import { displayErrorWithOutput } from './utils/errors' -import { ExtUri, FileUri, parseExtUri, toExtUri } from './utils/exturi' +import { ExtUri, parseExtUri, toExtUri } from './utils/exturi' import { fileExists } from './utils/fsHelper' +import { + displayError, + displayErrorWithOptionalInput, + displayErrorWithOutput, + displayInformationWithOptionalInput, +} from './utils/notifs' import path = require('path') const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&') @@ -69,7 +66,6 @@ export function getFullRange(diag: Diagnostic): Range { export class LeanClient implements Disposable { running: boolean private client: LanguageClient | undefined - private toolchainPath: string private outputChannel: OutputChannel folderUri: ExtUri private subscriptions: Disposable[] = [] @@ -123,8 +119,6 @@ export class LeanClient implements Disposable { this.outputChannel = outputChannel // can be null when opening adhoc files. this.folderUri = folderUri this.elanDefaultToolchain = elanDefaultToolchain - if (!this.toolchainPath) this.toolchainPath = toolchainPath() - this.subscriptions.push(workspace.onDidChangeConfiguration(e => this.configChanged(e))) this.subscriptions.push( new Disposable(() => { if (this.staleDepNotifier) { @@ -139,11 +133,14 @@ export class LeanClient implements Disposable { if (this.isStarted()) void this.stop() } - async showRestartMessage(restartFile: boolean = false, uri?: ExtUri | undefined): Promise { + showRestartMessage(restartFile: boolean = false, uri?: ExtUri | undefined) { if (this.showingRestartMessage) { return } this.showingRestartMessage = true + const finalizer = () => { + this.showingRestartMessage = false + } let restartItem: string let messageTitle: string if (!restartFile) { @@ -153,23 +150,26 @@ export class LeanClient implements Disposable { restartItem = 'Restart Lean Server on this file' messageTitle = 'The Lean Server has stopped processing this file.' } - const item = await window.showErrorMessage(messageTitle, restartItem) - this.showingRestartMessage = false - if (item === restartItem) { - if (restartFile && uri !== undefined) { - const document = workspace.textDocuments.find(doc => uri.equalsUri(doc.uri)) - if (document) { - await this.restartFile(document) + displayErrorWithOptionalInput( + messageTitle, + restartItem, + () => { + if (restartFile && uri !== undefined) { + const document = workspace.textDocuments.find(doc => uri.equalsUri(doc.uri)) + if (document) { + void this.restartFile(document) + } + } else { + void this.start() } - } else { - void this.start() - } - } + }, + finalizer, + ) } async restart(): Promise { if (this.isRestarting) { - await window.showErrorMessage('Client is already being started.') + displayError('Client is already being started.') return } this.isRestarting = true @@ -180,7 +180,6 @@ export class LeanClient implements Disposable { } this.restartingEmitter.fire(undefined) - this.toolchainPath = toolchainPath() const progressOptions: ProgressOptions = { location: ProgressLocation.Notification, @@ -220,7 +219,7 @@ export class LeanClient implements Disposable { // only raise this event and show the message if we are not the ones // who called the stop() method. this.stoppedEmitter.fire({ message: 'Lean server has stopped.', reason: '' }) - await this.showRestartMessage() + this.showRestartMessage() } } }) @@ -279,8 +278,10 @@ export class LeanClient implements Disposable { this.client?.outputChannel.show(true) } else if (!stderrMsgBoxVisible) { stderrMsgBoxVisible = true - await displayErrorWithOutput(`Lean server printed an error:\n${chunk.toString()}`) - stderrMsgBoxVisible = false + const finalizer = () => { + stderrMsgBoxVisible = false + } + displayErrorWithOutput(`Lean server printed an error:\n${chunk.toString()}`, finalizer) } }) @@ -288,7 +289,7 @@ export class LeanClient implements Disposable { insideRestart = false } - private async checkForImportsOutdatedError(params: PublishDiagnosticsParams) { + private checkForImportsOutdatedError(params: PublishDiagnosticsParams) { const fileUri = parseExtUri(params.uri) if (fileUri === undefined) { return @@ -310,18 +311,15 @@ export class LeanClient implements Disposable { const message = `Imports of '${fileName}' are out of date and must be rebuilt. Restarting the file will rebuild them.` const input = 'Restart File' - const choice = await window.showInformationMessage(message, input) - if (choice !== input) { - return - } - - const document = workspace.textDocuments.find(doc => fileUri.equalsUri(doc.uri)) - if (!document || document.isClosed) { - void window.showErrorMessage(`'${fileName}' was closed in the meantime. Imports will not be rebuilt.`) - return - } + displayInformationWithOptionalInput(message, input, () => { + const document = workspace.textDocuments.find(doc => fileUri.equalsUri(doc.uri)) + if (!document || document.isClosed) { + displayError(`'${fileName}' was closed in the meantime. Imports will not be rebuilt.`) + return + } - await this.restartFile(document) + void this.restartFile(document) + }) } async withStoppedClient(action: () => Promise): Promise<'Success' | 'IsRestarting'> { @@ -416,13 +414,6 @@ export class LeanClient implements Disposable { this.running = false } - configChanged(e: ConfigurationChangeEvent): void { - const newToolchainPath = toolchainPath() - if (this.toolchainPath !== newToolchainPath) { - void this.restart() - } - } - async restartFile(doc: TextDocument): Promise { if (!this.running) return // there was a problem starting lean server. @@ -484,60 +475,8 @@ export class LeanClient implements Disposable { return this.running ? this.client?.initializeResult : undefined } - private async checkToolchainVersion(folderUri: FileUri): Promise { - // see if we have a well known toolchain label that corresponds - // to a known date like 'leanprover/lean4:nightly-2022-02-01' - const toolchainVersion = await readLeanVersion(folderUri) - if (toolchainVersion) { - const nightly_match = /^leanprover\/lean4:nightly-(\d+)-(\d+)-(\d+)$/.exec(toolchainVersion) - if (nightly_match) { - return new Date(parseInt(nightly_match[1]), parseInt(nightly_match[2]) - 1, parseInt(nightly_match[3])) - } - const release_match = /^leanprover\/lean4:(\d+)-(\d+)-(\d+)$/.exec(toolchainVersion) - if (release_match) { - return new Date(2023, 9, 8) - } - if (toolchainVersion === 'leanprover/lean4:stable') { - return new Date(2022, 2, 1) - } - } - return undefined - } - - async checkLakeVersion(executable: string, version: string | null): Promise { - // Check that the Lake version is high enough to support "lake serve" option. - const versionOptions = version ? ['+' + version, '--version'] : ['--version'] - const start = Date.now() - const cwd = this.folderUri.scheme === 'file' ? this.folderUri.fsPath : undefined - const result: ExecutionResult = await batchExecute(executable, versionOptions, cwd) - if (result.exitCode !== ExecutionExitCode.Success) { - logger.error(`[LeanClient] Ran '${executable} ${versionOptions.join(' ')}', got error:\n${result.stderr}`) - return false - } - logger.log(`[LeanClient] Ran '${executable} ${versionOptions.join(' ')}' in ${Date.now() - start} ms`) - const lakeVersion = result.stdout - const actual = this.extractVersion(lakeVersion) - if (actual.compare('3.0.0') > 0) { - return true - } - return false - } - - private extractVersion(v: string | undefined): SemVer { - if (!v) return new SemVer('0.0.0') - const prefix = 'Lake version' - if (v.startsWith(prefix)) v = v.slice(prefix.length).trim() - const pos = v.indexOf('(') - if (pos > 0) v = v.slice(0, pos).trim() - try { - return new SemVer(v) - } catch { - return new SemVer('0.0.0') - } - } - private async determineServerOptions(): Promise { - const env = addServerEnvPaths(process.env) + const env = Object.assign({}, process.env) if (serverLoggingEnabled()) { env.LEAN_SERVER_LOG_DIR = serverLoggingPath() } @@ -566,36 +505,22 @@ export class LeanClient implements Disposable { } private async determineExecutable(): Promise<[string, string[]]> { - const lakeExecutable = lakePath() || (this.toolchainPath ? join(this.toolchainPath, 'bin', 'lake') : 'lake') - const leanExecutable = this.toolchainPath ? join(this.toolchainPath, 'bin', 'lean') : 'lean' - - if (await this.shouldUseLake(lakeExecutable)) { - return [lakeExecutable, ['serve', '--']] + if (await this.shouldUseLake()) { + return ['lake', ['serve', '--']] } else { - return [leanExecutable, ['--server']] + return ['lean', ['--server']] } } - private async shouldUseLake(lakeExecutable: string): Promise { + private async shouldUseLake(): Promise { // check if the lake process will start (skip it on scheme: 'untitled' files) - if (!lakeEnabled() || this.folderUri.scheme !== 'file') { + if (this.folderUri.scheme !== 'file') { return false } const lakefileLean = this.folderUri.join('lakefile.lean') const lakefileToml = this.folderUri.join('lakefile.toml') - if (!(await fileExists(lakefileLean.fsPath)) && !(await fileExists(lakefileToml.fsPath))) { - return false - } - - // see if we can avoid the more expensive checkLakeVersion call. - const date = await this.checkToolchainVersion(this.folderUri) - if (date) { - // Feb 16 2022 is when the 3.1.0.pre was released. - return date >= new Date(2022, 1, 16) - } - - return await this.checkLakeVersion(lakeExecutable, null) + return (await fileExists(lakefileLean.fsPath)) || (await fileExists(lakefileToml.fsPath)) } private obtainClientOptions(): LanguageClientOptions { diff --git a/vscode-lean4/src/projectDiagnostics.ts b/vscode-lean4/src/projectDiagnostics.ts new file mode 100644 index 000000000..3619b9be8 --- /dev/null +++ b/vscode-lean4/src/projectDiagnostics.ts @@ -0,0 +1,144 @@ +import { SemVer } from 'semver' +import { OutputChannel, commands } from 'vscode' +import { ExtUri, FileUri } from './utils/exturi' +import { + PreconditionCheckResult, + SetupDiagnoser, + diagnose, + displaySetupError, + displaySetupErrorWithOutput, + displaySetupWarning, + displaySetupWarningWithOptionalInput, + worstPreconditionViolation, +} from './utils/setupDiagnostics' + +const singleFileWarningMessage = `Lean 4 server is operating in restricted single file mode. +Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. +Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` + +const missingLeanToolchainWarningMessage = `Opened folder does not contain a valid Lean 4 project. +Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. +Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` + +const missingLeanToolchainWithParentProjectWarningMessage = (parentProjectFolder: FileUri) => + `Opened folder does not contain a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. +However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. +Open this project instead?` + +const lean3ProjectErrorMessage = (projectVersion: SemVer) => + `Opened file is using Lean 3 (version: ${projectVersion.toString()}). +If you want to use Lean 3, disable this extension ('Extensions' in the left sidebar > Cog icon on 'lean4' > 'Disable') and install the 'lean' extension for Lean 3 support.` + +const ancientLean4ProjectWarningMessage = (projectVersion: SemVer) => + `Opened file is using a Lean 4 version (${projectVersion.toString()}) from before the first Lean 4 stable release (4.0.0). +Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.` + +class ProjectDiagnosticsProvider { + readonly channel: OutputChannel + readonly folderUri: ExtUri + + constructor(channel: OutputChannel, folderUri: ExtUri) { + this.channel = channel + this.folderUri = folderUri + } + + private diagnose(): SetupDiagnoser { + const cwd = this.folderUri.scheme === 'file' ? this.folderUri : undefined + return diagnose(this.channel, cwd) + } + + async checkIsValidProjectFolder(): Promise { + const projectSetupDiagnosis = await this.diagnose().projectSetup() + switch (projectSetupDiagnosis.kind) { + case 'SingleFile': + displaySetupWarning(singleFileWarningMessage) + return false + + case 'MissingLeanToolchain': + const parentProjectFolder = projectSetupDiagnosis.parentProjectFolder + if (parentProjectFolder === undefined) { + displaySetupWarning(missingLeanToolchainWarningMessage) + } else { + displaySetupWarningWithOptionalInput( + missingLeanToolchainWithParentProjectWarningMessage(parentProjectFolder), + 'Open Parent Directory Project', + // this kills the extension host + () => commands.executeCommand('vscode.openFolder', parentProjectFolder), + ) + } + return false + + case 'ValidProjectSetup': + return true + } + } + + async checkIsLeanVersionUpToDate(): Promise { + const projectLeanVersionDiagnosis = await this.diagnose().projectLeanVersion() + switch (projectLeanVersionDiagnosis.kind) { + case 'NotInstalled': + displaySetupErrorWithOutput("Error while checking Lean version: 'lean' command was not found.") + return PreconditionCheckResult.Fatal + + case 'ExecutionError': + displaySetupErrorWithOutput(`Error while checking Lean version: ${projectLeanVersionDiagnosis.message}`) + return PreconditionCheckResult.Fatal + + case 'IsLean3Version': + void displaySetupError(lean3ProjectErrorMessage(projectLeanVersionDiagnosis.version)) + return PreconditionCheckResult.Fatal + + case 'IsAncientLean4Version': + displaySetupWarning(ancientLean4ProjectWarningMessage(projectLeanVersionDiagnosis.version)) + return PreconditionCheckResult.Warning + + case 'UpToDate': + return PreconditionCheckResult.Fulfilled + } + } + + async checkIsLakeInstalled(): Promise { + const lakeVersionResult = await this.diagnose().queryLakeVersion() + switch (lakeVersionResult.kind) { + case 'CommandNotFound': + displaySetupErrorWithOutput("Error while checking Lake version: 'lake' command was not found.") + return PreconditionCheckResult.Fatal + + case 'CommandError': + displaySetupErrorWithOutput(`Error while checking Lake version: ${lakeVersionResult.message}`) + return PreconditionCheckResult.Fatal + + case 'InvalidVersion': + displaySetupErrorWithOutput( + `Error while checking Lake version: Invalid Lake version format: '${lakeVersionResult.versionResult}'`, + ) + return PreconditionCheckResult.Fatal + + case 'Success': + return PreconditionCheckResult.Fulfilled + } + } +} + +export async function checkLean4ProjectPreconditions( + channel: OutputChannel, + folderUri: ExtUri, +): Promise { + const diagnosticsProvider = new ProjectDiagnosticsProvider(channel, folderUri) + + const isValidProjectFolder = await diagnosticsProvider.checkIsValidProjectFolder() + const validProjectFolderCheckResult = isValidProjectFolder + ? PreconditionCheckResult.Fulfilled + : PreconditionCheckResult.Warning + + const leanVersionCheckResult = await diagnosticsProvider.checkIsLeanVersionUpToDate() + + const leanProjectCheckResult = worstPreconditionViolation(validProjectFolderCheckResult, leanVersionCheckResult) + if (leanProjectCheckResult === PreconditionCheckResult.Fatal) { + return PreconditionCheckResult.Fatal + } + + const lakeVersionCheckResult = await diagnosticsProvider.checkIsLakeInstalled() + + return worstPreconditionViolation(leanProjectCheckResult, lakeVersionCheckResult) +} diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 9c9bfd969..6c6ffd562 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -1,8 +1,15 @@ import { commands, Disposable, OutputChannel, SaveDialogOptions, Uri, window, workspace } from 'vscode' -import { batchExecute, batchExecuteWithProgress, displayError, ExecutionExitCode, ExecutionResult } from './utils/batch' +import { + batchExecute, + batchExecuteWithProgress, + displayResultError, + ExecutionExitCode, + ExecutionResult, +} from './utils/batch' import { elanSelfUpdate } from './utils/elan' import { FileUri } from './utils/exturi' import { lake } from './utils/lake' +import { displayError, displayInformationWithInput } from './utils/notifs' import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo' import { diagnose } from './utils/setupDiagnostics' import path = require('path') @@ -31,7 +38,7 @@ export class ProjectInitializationProvider implements Disposable { return } if (buildResult.exitCode !== ExecutionExitCode.Success) { - await displayError(buildResult, 'Cannot build Lean project.') + displayResultError(buildResult, 'Cannot build Lean project.') return } @@ -60,7 +67,7 @@ export class ProjectInitializationProvider implements Disposable { return } if (cacheGetResult.exitCode !== ExecutionExitCode.Success) { - await displayError(cacheGetResult, 'Cannot fetch Mathlib build artifact cache.') + displayResultError(cacheGetResult, 'Cannot fetch Mathlib build artifact cache.') return } @@ -69,7 +76,7 @@ export class ProjectInitializationProvider implements Disposable { return } if (buildResult.exitCode !== ExecutionExitCode.Success) { - await displayError(buildResult, 'Cannot build Lean project.') + displayResultError(buildResult, 'Cannot build Lean project.') return } @@ -109,7 +116,7 @@ export class ProjectInitializationProvider implements Disposable { kind, ) if (result.exitCode !== ExecutionExitCode.Success) { - await displayError(result, 'Cannot initialize project.') + displayResultError(result, 'Cannot initialize project.') return 'DidNotComplete' } @@ -118,7 +125,7 @@ export class ProjectInitializationProvider implements Disposable { return 'DidNotComplete' } if (updateResult.exitCode !== ExecutionExitCode.Success) { - await displayError(updateResult, 'Cannot update dependencies.') + displayResultError(updateResult, 'Cannot update dependencies.') return 'DidNotComplete' } @@ -130,7 +137,7 @@ export class ProjectInitializationProvider implements Disposable { combined: this.channel, }) if (gitAddResult.exitCode !== ExecutionExitCode.Success) { - await displayError(gitAddResult, 'Cannot add files to staging area of Git repository for project.') + displayResultError(gitAddResult, 'Cannot add files to staging area of Git repository for project.') return 'GitAddFailed' } @@ -141,7 +148,7 @@ export class ProjectInitializationProvider implements Disposable { { combined: this.channel }, ) if (gitCommitResult.exitCode !== ExecutionExitCode.Success) { - await displayError(gitAddResult, 'Cannot commit files to Git repository for project.') + displayResultError(gitAddResult, 'Cannot commit files to Git repository for project.') return 'GitCommitFailed' } @@ -185,7 +192,7 @@ export class ProjectInitializationProvider implements Disposable { const message = `The selected folder is not a valid Lean 4 project folder. Please make sure to select a folder containing a \'lean-toolchain\' file. Click the following link to learn how to set up Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - void window.showErrorMessage(message) + displayError(message) return undefined } @@ -193,7 +200,7 @@ Click the following link to learn how to set up Lean projects: [(Show Setup Guid However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. Open this project instead?` const input = 'Open parent directory project' - const choice: string | undefined = await window.showInformationMessage(message, { modal: true }, input) + const choice: string | undefined = await displayInformationWithInput(message, input) if (choice !== input) { return undefined } @@ -233,7 +240,7 @@ Open this project instead?` return } if (result.exitCode !== ExecutionExitCode.Success) { - await displayError(result, 'Cannot download project.') + displayResultError(result, 'Cannot download project.') return } @@ -262,7 +269,7 @@ Open this project instead?` if (projectFolder.scheme === 'file') { return true } else { - void window.showErrorMessage('Project folder must be created in a file system.') + displayError('Project folder must be created in a file system.') return false } } @@ -270,7 +277,7 @@ Open this project instead?` private static async openNewFolder(projectFolder: FileUri) { const message = `Project initialized. Open new project folder '${path.basename(projectFolder.fsPath)}'?` const input = 'Open project folder' - const choice: string | undefined = await window.showInformationMessage(message, { modal: true }, input) + const choice: string | undefined = await displayInformationWithInput(message, input) if (choice === input) { // This kills the extension host, so it has to be the last command await commands.executeCommand('vscode.openFolder', projectFolder.asUri()) @@ -291,7 +298,7 @@ Open this project instead?` if (!(await diagnose(this.channel, projectFolder).checkGitAvailable())) { const message = `Git is not installed. Lean uses Git to download and install specific versions of Lean packages. Click the following link to learn how to install Git: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - void window.showErrorMessage(message) + displayError(message) return 'GitNotInstalled' } return 'GitInstalled' @@ -301,7 +308,7 @@ Click the following link to learn how to install Git: [(Show Setup Guide)](comma if (!(await diagnose(this.channel, projectFolder).checkLakeAvailable())) { const message = `Lean's package manager Lake is not installed. This likely means that Lean itself is also not installed. Click the following link to learn how to install Lean: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - void window.showErrorMessage(message) + displayError(message) return 'LakeNotInstalled' } return 'LakeInstalled' diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts index b1b1319af..947a58af6 100644 --- a/vscode-lean4/src/projectoperations.ts +++ b/vscode-lean4/src/projectoperations.ts @@ -2,10 +2,11 @@ import * as fs from 'fs' import { join } from 'path' import { commands, Disposable, OutputChannel, QuickPickItem, window } from 'vscode' import { LeanClient } from './leanclient' -import { batchExecute, displayError, ExecutionExitCode, ExecutionResult } from './utils/batch' +import { batchExecute, displayResultError, ExecutionExitCode, ExecutionResult } from './utils/batch' import { LeanClientProvider } from './utils/clientProvider' import { cacheNotFoundError, lake, LakeRunner } from './utils/lake' import { DirectGitDependency, Manifest, ManifestReadError, parseManifestInFolder } from './utils/manifest' +import { displayError, displayInformation, displayInformationWithInput, displayWarningWithInput } from './utils/notifs' export class ProjectOperationProvider implements Disposable { private subscriptions: Disposable[] = [] @@ -35,20 +36,19 @@ export class ProjectOperationProvider implements Disposable { return } if (result.exitCode !== ExecutionExitCode.Success) { - void displayError(result, 'Cannot build project.') + displayResultError(result, 'Cannot build project.') return } - void window.showInformationMessage('Project built successfully.') + displayInformation('Project built successfully.') return }) } private async cleanProject() { const deleteInput = 'Proceed' - const deleteChoice: string | undefined = await window.showInformationMessage( + const deleteChoice: string | undefined = await displayInformationWithInput( 'Delete all build artifacts?', - { modal: true }, deleteInput, ) if (deleteChoice !== deleteInput) { @@ -61,7 +61,7 @@ export class ProjectOperationProvider implements Disposable { return } if (cleanResult.exitCode !== ExecutionExitCode.Success) { - void displayError(cleanResult, 'Cannot delete build artifacts.') + displayResultError(cleanResult, 'Cannot delete build artifacts.') return } @@ -70,17 +70,13 @@ export class ProjectOperationProvider implements Disposable { return } if (checkResult === 'No') { - void window.showInformationMessage('Project cleaned successfully.') + displayInformation('Project cleaned successfully.') return } const fetchMessage = "Project cleaned successfully. Do you want to fetch Mathlib's build artifact cache?" const fetchInput = 'Fetch Cache' - const fetchChoice: string | undefined = await window.showInformationMessage( - fetchMessage, - { modal: true }, - fetchInput, - ) + const fetchChoice: string | undefined = await displayInformationWithInput(fetchMessage, fetchInput) if (fetchChoice !== fetchInput) { return } @@ -90,10 +86,10 @@ export class ProjectOperationProvider implements Disposable { return } if (fetchResult.exitCode !== ExecutionExitCode.Success) { - void displayError(fetchResult, 'Cannot fetch Mathlib build artifact cache.') + void displayResultError(fetchResult, 'Cannot fetch Mathlib build artifact cache.') return } - void window.showInformationMessage('Mathlib build artifact cache fetched successfully.') + displayInformation('Mathlib build artifact cache fetched successfully.') }) } @@ -105,41 +101,41 @@ export class ProjectOperationProvider implements Disposable { } if (result.exitCode !== ExecutionExitCode.Success) { if (result.stderr.includes(cacheNotFoundError)) { - void window.showErrorMessage('This command cannot be used in non-Mathlib projects.') + displayError('This command cannot be used in non-Mathlib projects.') return } - void displayError(result, 'Cannot fetch Mathlib build artifact cache.') + displayResultError(result, 'Cannot fetch Mathlib build artifact cache.') return } - void window.showInformationMessage('Mathlib build artifact cache fetched successfully.') + displayInformation('Mathlib build artifact cache fetched successfully.') }) } private async updateDependency() { const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient() if (!activeClient) { - void window.showErrorMessage('No active client.') + displayError('No active client.') return } const activeFolderUri = activeClient.folderUri if (activeFolderUri.scheme === 'untitled') { - void window.showErrorMessage('Cannot update dependency of untitled file.') + displayError('Cannot update dependency of untitled file.') return } const manifestResult: Manifest | ManifestReadError = await parseManifestInFolder(activeFolderUri) if (typeof manifestResult === 'string') { - void window.showErrorMessage(manifestResult) + displayError(manifestResult) return } const dependencies: (DirectGitDependency & { remoteRevision?: string | undefined })[] = await this.findUpdateableDependencies(manifestResult.directGitDependencies) if (dependencies.length === 0) { - void window.showInformationMessage('Nothing to update - all dependencies are up-to-date.') + displayInformation('Nothing to update - all dependencies are up-to-date.') return } @@ -169,7 +165,7 @@ export class ProjectOperationProvider implements Disposable { const warningMessage = `This command will update ${dependencyChoice.name} to its most recent version. It is only intended to be used by maintainers of this project. If the updated version of ${dependencyChoice.name} is incompatible with any other dependency or the code in this project, this project may not successfully build anymore. Are you sure you want to proceed?` const warningInput = 'Proceed' - const warningChoice = await window.showWarningMessage(warningMessage, { modal: true }, warningInput) + const warningChoice = await displayWarningWithInput(warningMessage, warningInput) if (warningChoice !== warningInput) { return } @@ -180,7 +176,7 @@ export class ProjectOperationProvider implements Disposable { return } if (result.exitCode !== ExecutionExitCode.Success) { - void displayError(result, 'Cannot update dependency.') + void displayResultError(result, 'Cannot update dependency.') return } @@ -207,7 +203,7 @@ export class ProjectOperationProvider implements Disposable { try { fs.writeFileSync(localToolchainPath, dependencyToolchainResult) } catch { - void window.showErrorMessage('Cannot update Lean version.') + displayError('Cannot update Lean version.') return } } @@ -259,7 +255,7 @@ export class ProjectOperationProvider implements Disposable { : `Could not read Lean version of ${dependencyName} at ${dependencyToolchainPath}` const message = `${errorFlavor}. Do you want to update ${dependencyName} without updating the Lean version of the open project to that of ${dependencyName} regardless?` const input = 'Proceed' - const choice: string | undefined = await window.showInformationMessage(message, { modal: true }, input) + const choice: string | undefined = await displayInformationWithInput(message, input) return choice === 'input' ? 'DoNotUpdate' : 'Cancelled' } const [localToolchain, dependencyToolchain]: [string, string] = toolchainResult @@ -271,7 +267,7 @@ export class ProjectOperationProvider implements Disposable { const message = `The Lean version '${localToolchain}' of the open project differs from the Lean version '${dependencyToolchain}' of ${dependencyName}. Do you want to update the Lean version of the open project to the Lean version of ${dependencyName}?` const input1 = 'Update Lean Version' const input2 = 'Keep Lean Version' - const choice = await window.showInformationMessage(message, { modal: true }, input1, input2) + const choice = await displayInformationWithInput(message, input1, input2) if (choice === undefined) { return 'Cancelled' } @@ -317,28 +313,26 @@ export class ProjectOperationProvider implements Disposable { private async runOperation(command: (lakeRunner: LakeRunner) => Promise) { if (this.isRunningOperation) { - void window.showErrorMessage( - 'Another project action is already being executed. Please wait for its completion.', - ) + displayError('Another project action is already being executed. Please wait for its completion.') return } this.isRunningOperation = true if (!this.clientProvider) { - void window.showErrorMessage('Lean client has not loaded yet.') + displayError('Lean client has not loaded yet.') this.isRunningOperation = false return } const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient() if (!activeClient) { - void window.showErrorMessage('No active client.') + displayError('No active client.') this.isRunningOperation = false return } if (activeClient.folderUri.scheme === 'untitled') { - void window.showErrorMessage('Cannot run project action for untitled files.') + displayError('Cannot run project action for untitled files.') this.isRunningOperation = false return } @@ -347,7 +341,7 @@ export class ProjectOperationProvider implements Disposable { const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner)) if (result === 'IsRestarting') { - void window.showErrorMessage('Cannot run project action while restarting the server.') + displayError('Cannot run project action while restarting the server.') } this.isRunningOperation = false diff --git a/vscode-lean4/src/utils/batch.ts b/vscode-lean4/src/utils/batch.ts index 2e2366744..15e2db3f9 100644 --- a/vscode-lean4/src/utils/batch.ts +++ b/vscode-lean4/src/utils/batch.ts @@ -1,8 +1,7 @@ -import { spawn } from 'child_process' -import { CancellationToken, Disposable, OutputChannel, ProgressLocation, ProgressOptions, window } from 'vscode' -import { findProgramInPath, isRunningTest } from '../config' -import { displayErrorWithOutput } from './errors' +import { ChildProcessWithoutNullStreams, spawn } from 'child_process' +import { OutputChannel, Progress, ProgressLocation, ProgressOptions, window } from 'vscode' import { logger } from './logger' +import { displayErrorWithOutput } from './notifs' export interface ExecutionChannel { combined?: OutputChannel | undefined @@ -21,109 +20,121 @@ export interface ExecutionResult { exitCode: ExecutionExitCode stdout: string stderr: string + combined: string } function createCannotLaunchExecutionResult(message: string): ExecutionResult { return { exitCode: ExecutionExitCode.CannotLaunch, - stdout: '', - stderr: message, + stdout: message, + stderr: '', + combined: message, } } -export async function batchExecute( +export function batchExecuteWithProc( executablePath: string, args: string[], workingDirectory?: string | undefined, channel?: ExecutionChannel | undefined, - token?: CancellationToken | undefined, -): Promise { - return new Promise(function (resolve, reject) { - let stdout: string = '' - let stderr: string = '' - let options = {} - if (workingDirectory !== undefined) { - options = { cwd: workingDirectory } - } - - try { - if (isRunningTest()) { - // The mocha test framework listens to process.on('uncaughtException') - // which is raised if spawn cannot find the command and the test automatically - // fails with "Uncaught Error: spawn elan ENOENT". Therefore we manually - // check if the command exists so as not to trigger that exception. - const fullPath = findProgramInPath(executablePath) - if (!fullPath) { - resolve(createCannotLaunchExecutionResult('')) - return - } - } - if (channel?.combined) { - const formattedCwd = workingDirectory ? `${workingDirectory}` : '' - const formattedArgs = args.map(arg => (arg.includes(' ') ? `"${arg}"` : arg)).join(' ') - channel.combined.appendLine(`${formattedCwd}> ${executablePath} ${formattedArgs}`) - } - const proc = spawn(executablePath, args, options) +): [ChildProcessWithoutNullStreams | 'CannotLaunch', Promise] { + let stdout: string = '' + let stderr: string = '' + let combined: string = '' + let options = {} + if (workingDirectory !== undefined) { + options = { cwd: workingDirectory } + } + if (channel?.combined) { + const formattedCwd = workingDirectory ? `${workingDirectory}` : '' + const formattedArgs = args.map(arg => (arg.includes(' ') ? `"${arg}"` : arg)).join(' ') + channel.combined.appendLine(`${formattedCwd}> ${executablePath} ${formattedArgs}`) + } - const disposeKill: Disposable | undefined = token?.onCancellationRequested(_ => proc.kill()) + let proc: ChildProcessWithoutNullStreams + try { + proc = spawn(executablePath, args, options) + } catch (e) { + return ['CannotLaunch', new Promise(resolve => resolve(createCannotLaunchExecutionResult('')))] + } - proc.on('error', err => { - disposeKill?.dispose() - resolve(createCannotLaunchExecutionResult(err.message)) + const execPromise: Promise = new Promise(resolve => { + const conclude = (r: ExecutionResult) => + resolve({ + exitCode: r.exitCode, + stdout: r.stdout.trim(), + stderr: r.stderr.trim(), + combined: r.combined.trim(), }) - proc.stdout.on('data', line => { - const s: string = line.toString() - if (channel?.combined) channel.combined.appendLine(s) - if (channel?.stdout) channel.stdout.appendLine(s) - stdout += s + '\n' - }) + proc.on('error', err => { + conclude(createCannotLaunchExecutionResult(err.message)) + }) - proc.stderr.on('data', line => { - const s: string = line.toString() - if (channel?.combined) channel.combined.appendLine(s) - if (channel?.stderr) channel.stderr.appendLine(s) - stderr += s + '\n' - }) + proc.stdout.on('data', line => { + const s: string = line.toString() + if (channel?.combined) channel.combined.appendLine(s) + if (channel?.stdout) channel.stdout.appendLine(s) + stdout += s + '\n' + combined += s + '\n' + }) - proc.on('close', (code, signal) => { - disposeKill?.dispose() - logger.log(`child process exited with code ${code}`) - if (signal === 'SIGTERM') { - if (channel?.combined) { - channel.combined.appendLine('=> Operation cancelled by user.') - } - resolve({ - exitCode: ExecutionExitCode.Cancelled, - stdout, - stderr, - }) - return + proc.stderr.on('data', line => { + const s: string = line.toString() + if (channel?.combined) channel.combined.appendLine(s) + if (channel?.stderr) channel.stderr.appendLine(s) + stderr += s + '\n' + combined += s + '\n' + }) + + proc.on('close', (code, signal) => { + logger.log(`child process exited with code ${code}`) + if (signal === 'SIGTERM') { + if (channel?.combined) { + channel.combined.appendLine('=> Operation cancelled by user.') } - if (code !== 0) { - if (channel?.combined) { - const formattedCode = code ? `Exit code: ${code}.` : '' - const formattedSignal = signal ? `Signal: ${signal}.` : '' - channel.combined.appendLine(`=> Operation failed. ${formattedCode} ${formattedSignal}`.trim()) - } - resolve({ - exitCode: ExecutionExitCode.ExecutionError, - stdout, - stderr, - }) - return + conclude({ + exitCode: ExecutionExitCode.Cancelled, + stdout, + stderr, + combined, + }) + return + } + if (code !== 0) { + if (channel?.combined) { + const formattedCode = code ? `Exit code: ${code}.` : '' + const formattedSignal = signal ? `Signal: ${signal}.` : '' + channel.combined.appendLine(`=> Operation failed. ${formattedCode} ${formattedSignal}`.trim()) } - resolve({ - exitCode: ExecutionExitCode.Success, + conclude({ + exitCode: ExecutionExitCode.ExecutionError, stdout, stderr, + combined, }) + return + } + conclude({ + exitCode: ExecutionExitCode.Success, + stdout, + stderr, + combined, }) - } catch (e) { - logger.log(`error running ${executablePath} : ${e}`) - resolve(createCannotLaunchExecutionResult('')) - } + }) }) + + return [proc, execPromise] +} + +export async function batchExecute( + executablePath: string, + args: string[], + workingDirectory?: string | undefined, + channel?: ExecutionChannel | undefined, +): Promise { + const [_, execPromise] = batchExecuteWithProc(executablePath, args, workingDirectory, channel) + return execPromise } interface ProgressExecutionOptions { @@ -146,48 +157,78 @@ export async function batchExecuteWithProgress( title: title + titleSuffix, cancellable: options.allowCancellation === true, } + let inc = 0 + let lastReportedMessage: string | undefined + let progress: + | Progress<{ + message?: string | undefined + increment?: number | undefined + }> + | undefined - const result: ExecutionResult = await window.withProgress(progressOptions, (progress, token) => { - const progressChannel: OutputChannel = { - name: 'ProgressChannel', - append(value: string) { - if (options.translator) { - const translatedValue: string | undefined = options.translator(value) - if (translatedValue === undefined) { - return - } - value = translatedValue - } - if (options.channel) { - options.channel.appendLine(value.trimEnd()) - } - if (inc < 90) { - inc += 2 + const progressChannel: OutputChannel = { + name: 'ProgressChannel', + append(value: string) { + if (options.translator) { + const translatedValue: string | undefined = options.translator(value) + if (translatedValue === undefined) { + return } + value = translatedValue + } + if (options.channel) { + options.channel.appendLine(value.trimEnd()) + } + if (inc < 90) { + inc += 2 + } + if (progress !== undefined) { progress.report({ increment: inc, message: value }) - }, - appendLine(value: string) { - this.append(value + '\n') - }, - replace(_: string) { - /* empty */ - }, - clear() { - /* empty */ - }, - show() { - /* empty */ - }, - hide() { - /* empty */ - }, - dispose() { - /* empty */ - }, - } - progress.report({ increment: 0 }) - return batchExecute(executablePath, args, options.cwd, { combined: progressChannel }, token) + } + lastReportedMessage = value + }, + appendLine(value: string) { + this.append(value + '\n') + }, + replace(_: string) { + /* empty */ + }, + clear() { + /* empty */ + }, + show() { + /* empty */ + }, + hide() { + /* empty */ + }, + dispose() { + /* empty */ + }, + } + + const expensiveExecutionTimeoutPromise: Promise = new Promise((resolve, _) => + setTimeout(() => resolve(undefined), 250), + ) + const [proc, executionPromise] = batchExecuteWithProc(executablePath, args, options.cwd, { + combined: progressChannel, + }) + if (proc === 'CannotLaunch') { + return executionPromise // resolves to a 'CannotLaunch' ExecutionResult + } + + const preliminaryResult = await Promise.race([expensiveExecutionTimeoutPromise, executionPromise]) + if (preliminaryResult !== undefined) { + return preliminaryResult + } + + // Execution already took longer than 250ms, let's start displaying a progress bar now + const result: ExecutionResult = await window.withProgress(progressOptions, (p, token) => { + progress = p + token.onCancellationRequested(() => proc.kill()) + progress.report({ message: lastReportedMessage, increment: inc }) + return executionPromise }) return result } @@ -211,17 +252,17 @@ export async function executeAll(executions: BatchExecution[]): Promise = new Map() private clients: Map = new Map() private pending: Map = new Map() - private pendingInstallChanged: ExtUri[] = [] + private pendingInstallChanged: FileUri[] = [] private processingInstallChanged: boolean = false private activeClient: LeanClient | undefined = undefined @@ -43,7 +37,7 @@ export class LeanClientProvider implements Disposable { this.installer = installer // we must setup the installChanged event handler first before any didOpenEditor calls. - installer.installChanged(async (uri: ExtUri) => await this.onInstallChanged(uri)) + installer.installChanged(async (uri: FileUri) => await this.onInstallChanged(uri)) window.visibleTextEditors.forEach(e => this.didOpenEditor(e.document)) this.subscriptions.push( @@ -76,7 +70,6 @@ export class LeanClientProvider implements Disposable { logger.log(`[ClientProvider] onDidChangeWorkspaceFolders removing client for ${key}`) this.clients.delete(key) - this.versions.delete(key) client.dispose() this.clientRemovedEmitter.fire(client) }) @@ -87,16 +80,7 @@ export class LeanClientProvider implements Disposable { return this.activeClient } - private async findPackageRootUri(uri: ExtUri): Promise { - if (uri.scheme === 'file') { - const [root, _] = await findLeanPackageRoot(uri) - return root - } else { - return new UntitledUri() - } - } - - private async onInstallChanged(uri: ExtUri) { + private async onInstallChanged(uri: FileUri) { // Uri is a package Uri in the case a lean package file was changed. logger.log(`[ClientProvider] installChanged for ${uri}`) this.pendingInstallChanged.push(uri) @@ -112,20 +96,16 @@ export class LeanClientProvider implements Disposable { break } try { - // have to check again here in case elan install had --default-toolchain none. - const packageUri = await this.findPackageRootUri(uri) + const projectUri = await findLeanProjectRoot(uri) - logger.log('[ClientProvider] testLeanVersion') - const version = await this.installer.testLeanVersion(packageUri) - if (version.version === '4') { + const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, projectUri) + if (preconditionCheckResult !== PreconditionCheckResult.Fatal) { logger.log('[ClientProvider] got lean version 4') - const [cached, client] = await this.ensureClient(uri, version) + const [cached, client] = await this.ensureClient(uri) if (cached && client) { await client.restart() logger.log('[ClientProvider] restart complete') } - } else if (version.error) { - logger.log(`[ClientProvider] Lean version not ok: ${version.error}`) } } catch (e) { logger.log(`[ClientProvider] Exception checking lean version: ${e}`) @@ -134,20 +114,6 @@ export class LeanClientProvider implements Disposable { this.processingInstallChanged = false } - private async autoInstall(): Promise { - // no prompt, just do it! - await this.installer.installElan() - if (isElanDisabled()) { - addToolchainBinPath(getDefaultElanPath()) - } else { - addDefaultElanPath() - } - - for (const [_, client] of this.clients) { - await this.onInstallChanged(client.folderUri) - } - } - private getVisibleEditor(uri: ExtUri): TextEditor | undefined { for (const editor of window.visibleTextEditors) { if (uri.equalsUri(editor.document.uri)) { @@ -159,12 +125,12 @@ export class LeanClientProvider implements Disposable { private restartFile() { if (!this.activeClient || !this.activeClient.isRunning()) { - void window.showErrorMessage('No active client.') + displayError('No active client.') return } if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') { - void window.showErrorMessage( + displayError( 'No active Lean editor tab. Make sure to focus the Lean editor tab for which you want to issue a restart.', ) return @@ -207,14 +173,12 @@ export class LeanClientProvider implements Disposable { } try { - const [cached, client] = await this.ensureClient(uri, undefined) + const [_, client] = await this.ensureClient(uri) if (!client) { return } await client.openLean4Document(document) - - await this.checkIsValidProjectFolder(client.folderUri) } catch (e) { logger.log(`[ClientProvider] ### Error opening document: ${e}`) } @@ -252,157 +216,60 @@ export class LeanClientProvider implements Disposable { return this.clients.get(folder.toString()) } - private async getLeanVersion(uri: ExtUri): Promise { - const folderUri = await this.findPackageRootUri(uri) - const key = folderUri.toString() - if (this.versions.has(key)) { - return this.versions.get(key) - } - let versionInfo: LeanVersion | undefined = await this.installer.testLeanVersion(folderUri) - if (!versionInfo.error) { - this.versions.set(key, versionInfo) - } else if (versionInfo.error === 'no elan installed' || versionInfo.error === 'lean not found') { - if (!this.installer.getPromptUser()) { - await this.autoInstall() - versionInfo = await this.installer.testLeanVersion(folderUri) - if (!versionInfo.error) { - this.versions.set(key, versionInfo) - } - } else { - // Ah, then we need to prompt the user, this waits for answer, - // but does not wait for the install to complete. - await this.installer.showInstallOptions(uri) - } - } else { - void displayErrorWithOutput('Cannot determine Lean version: ' + versionInfo.error) - } - return versionInfo - } - // Starts a LeanClient if the given file is in a new workspace we haven't seen before. // Returns a boolean "true" if the LeanClient was already created. // Returns a null client if it turns out the new workspace is a lean3 workspace. - async ensureClient(uri: ExtUri, versionInfo: LeanVersion | undefined): Promise<[boolean, LeanClient | undefined]> { - const folderUri = await this.findPackageRootUri(uri) + async ensureClient(uri: ExtUri): Promise<[boolean, LeanClient | undefined]> { + const folderUri = uri.scheme === 'file' ? await findLeanProjectRoot(uri) : new UntitledUri() let client = this.getClientForFolder(folderUri) - const key = folderUri.toString() - const cachedClient = client !== undefined - if (!client) { - if (this.pending.has(key)) { - logger.log('[ClientProvider] ignoring ensureClient already pending on ' + folderUri.toString()) - return [cachedClient, client] - } - - this.pending.set(key, true) - if (!versionInfo) { - // this can go all the way to installing elan (in the test scenario) - // so it has to be done BEFORE we attempt to create any LeanClient. - versionInfo = await this.getLeanVersion(folderUri) - } - - logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString()) - const elanDefaultToolchain = await this.installer.getElanDefaultToolchain(folderUri) - - // We must create a Client before doing the long running testLeanVersion - // so that ensureClient callers have an "optimistic" client to work with. - // This is needed in our constructor where it is calling ensureClient for - // every open file. A workspace could have multiple files open and we want - // to remember all those open files are associated with this client before - // testLeanVersion has completed. - client = new LeanClient(folderUri, this.outputChannel, elanDefaultToolchain) - this.subscriptions.push(client) - this.clients.set(key, client) - - if (versionInfo && versionInfo.version && versionInfo.version !== '4') { - // ignore workspaces that belong to a different version of Lean. - logger.log( - `[ClientProvider] Lean4 extension ignoring workspace '${folderUri}' because it is not a Lean 4 workspace.`, - ) - this.pending.delete(key) - this.clients.delete(key) - client.dispose() - return [false, undefined] - } - - client.serverFailed(err => { - // forget this client! - logger.log(`[ClientProvider] serverFailed, removing client for ${key}`) - const cached = this.clients.get(key) - this.clients.delete(key) - cached?.dispose() - void window.showErrorMessage(err) - }) - - client.stopped(reason => { - if (client) { - // fires a message in case a client is stopped unexpectedly - this.clientStoppedEmitter.fire([client, client === this.activeClient, reason]) - } - }) + if (client) { + this.activeClient = client + return [true, client] + } - // aggregate progress changed events. - client.progressChanged(arg => { - this.progressChangedEmitter.fire(arg) - }) + const key = folderUri.toString() + if (this.pending.has(key)) { + return [false, undefined] + } + this.pending.set(key, true) + const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, folderUri) + if (preconditionCheckResult === PreconditionCheckResult.Fatal) { this.pending.delete(key) - logger.log('[ClientProvider] firing clientAddedEmitter event') - this.clientAddedEmitter.fire(client) - - if (versionInfo) { - if (!versionInfo.error) { - // we are ready to start, otherwise some sort of install might be happening - // as a result of UI options shown by testLeanVersion. - await client.start() - } else { - logger.log( - `[ClientProvider] skipping client.start because of versionInfo error: ${versionInfo?.error}`, - ) - } - } + return [false, undefined] } - // tell the InfoView about this activated client. - this.activeClient = client + logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString()) + const elanDefaultToolchain = await this.installer.getElanDefaultToolchain(folderUri) - return [cachedClient, client] - } + client = new LeanClient(folderUri, this.outputChannel, elanDefaultToolchain) + this.subscriptions.push(client) + this.clients.set(key, client) - private async checkIsValidProjectFolder(folderUri: ExtUri) { - if (!shouldShowInvalidProjectWarnings()) { - return - } + client.serverFailed(err => { + this.clients.delete(key) + client.dispose() + displayError(err) + }) - if (folderUri.scheme !== 'file') { - const message = `Lean 4 server operating in restricted single file mode. -Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. -Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - void window.showWarningMessage(message) - return - } + client.stopped(reason => { + this.clientStoppedEmitter.fire([client, client === this.activeClient, reason]) + }) - if (await isValidLeanProject(folderUri)) { - return - } + // aggregate progress changed events. + client.progressChanged(arg => { + this.progressChangedEmitter.fire(arg) + }) - const parentProjectFolder: FileUri | undefined = await checkParentFoldersForLeanProject(folderUri) - if (parentProjectFolder === undefined) { - const message = `Opened folder is not a valid Lean 4 project. -Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. -Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - void window.showWarningMessage(message) - return - } + this.pending.delete(key) + this.clientAddedEmitter.fire(client) - const message = `Opened folder is not a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. -However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. -Open this project instead?` - const input = 'Open parent directory project' - const choice: string | undefined = await window.showWarningMessage(message, input) - if (choice === input) { - // this kills the extension host - await commands.executeCommand('vscode.openFolder', parentProjectFolder) - } + await client.start() + + // tell the InfoView about this activated client. + this.activeClient = client + + return [false, client] } dispose(): void { diff --git a/vscode-lean4/src/utils/configwatchservice.ts b/vscode-lean4/src/utils/configwatchservice.ts index e3e30bc73..d46717e74 100644 --- a/vscode-lean4/src/utils/configwatchservice.ts +++ b/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 { findLeanPackageRoot, findLeanPackageVersionInfo } 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,7 +78,7 @@ 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 [packageUri, _] = await findLeanPackageRoot(fileUri) + const [packageUri, _] = await findLeanProjectRootInfo(fileUri) if (!packageUri) { return } @@ -108,7 +108,7 @@ export class LeanConfigWatchService implements Disposable { // note: apply the same rules here with findLeanPackageVersionInfo no matter // if a file is added or removed so we always match the elan behavior. - const [packageUri, version] = await findLeanPackageVersionInfo(fileUri) + const [packageUri, version] = await findLeanProjectInfo(fileUri) if (!packageUri || !version) { return } diff --git a/vscode-lean4/src/utils/envPath.ts b/vscode-lean4/src/utils/envPath.ts new file mode 100644 index 000000000..5423cbe73 --- /dev/null +++ b/vscode-lean4/src/utils/envPath.ts @@ -0,0 +1,70 @@ +import * as path from 'path' + +/** Platform independent interface to work with the PATH variable. */ +export class PATH { + paths: string[] + + constructor(paths: string[]) { + this.paths = paths + } + + static empty() { + return new PATH([]) + } + + static ofEnvPath(envPath: string): PATH { + return new PATH(envPath.split(path.delimiter)) + } + + static ofEnv(env: NodeJS.ProcessEnv): PATH { + return PATH.ofEnvPath(env.PATH ?? '') + } + + static ofProcessEnv(): PATH { + return PATH.ofEnv(process.env) + } + + toEnvPath(): string { + return this.paths.join(path.delimiter) + } + + setInEnv(env: NodeJS.ProcessEnv) { + env.PATH = this.toEnvPath() + } + + setInProcessEnv() { + this.setInEnv(process.env) + } + + prepend(path: string): PATH { + return new PATH([path].concat(this.paths)) + } + + join(other: PATH): PATH { + return new PATH(this.paths.concat(other.paths)) + } + + length(): number { + return this.paths.length + } + + isEmpty(): boolean { + return this.length() === 0 + } + + includes(path: string): boolean { + return this.paths.includes(path) + } + + filter(p: (path: string) => boolean): PATH { + return new PATH(this.paths.filter(p)) + } +} + +export function setPATH(env: NodeJS.ProcessEnv, path: PATH) { + path.setInEnv(env) +} + +export function setProcessEnvPATH(path: PATH) { + setPATH(process.env, path) +} diff --git a/vscode-lean4/src/utils/errors.ts b/vscode-lean4/src/utils/errors.ts deleted file mode 100644 index 376c41faa..000000000 --- a/vscode-lean4/src/utils/errors.ts +++ /dev/null @@ -1,9 +0,0 @@ -import { commands, window } from 'vscode' - -export async function displayErrorWithOutput(message: string) { - const input = 'Show Output' - const choice = await window.showErrorMessage(message, input) - if (choice === input) { - await commands.executeCommand('lean4.troubleshooting.showOutput') - } -} diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts index 39e737ebb..391198dc6 100644 --- a/vscode-lean4/src/utils/exturi.ts +++ b/vscode-lean4/src/utils/exturi.ts @@ -147,3 +147,13 @@ export function parseExtUri(uriString: string): ExtUri | undefined { export function parseExtUriOrError(uriString: string): ExtUri { return toExtUriOrError(Uri.parse(uriString)) } + +export function extUriEquals(a: ExtUri, b: ExtUri): boolean { + if (a.scheme === 'untitled' && b.scheme === 'untitled') { + return a.equals(b) + } + if (a.scheme === 'file' && b.scheme === 'file') { + return a.equals(b) + } + return false +} diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index fca5d6417..f80d11f01 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -1,10 +1,9 @@ -import { join } from 'path' import { EventEmitter, OutputChannel, TerminalOptions, window } from 'vscode' -import { addServerEnvPaths, getPowerShellPath, isRunningTest, shouldAutofocusOutput, toolchainPath } from '../config' -import { batchExecute, ExecutionExitCode, ExecutionResult } from './batch' +import { getPowerShellPath, isRunningTest } from '../config' +import { batchExecute } from './batch' import { ExtUri, FileUri } from './exturi' import { logger } from './logger' -import { isCoreLean4Directory, readLeanVersion } from './projectInfo' +import { displayError, displayErrorWithOptionalInput } from './notifs' export class LeanVersion { version: string @@ -16,21 +15,21 @@ export class LeanInstaller { private leanInstallerWindows = 'https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1' private outputChannel: OutputChannel private prompting: boolean = false - private defaultToolchain: string // the default to use if there is no elan installed + private installing: boolean = false + private freshInstallDefaultToolchain: string private elanDefaultToolchain: string = '' // the default toolchain according to elan (toolchain marked with '(default)') private workspaceSuffix: string = '(workspace override)' private defaultSuffix: string = '(default)' - private versionCache: Map = new Map() private promptUser: boolean = true // This event is raised whenever a version change happens. // The event provides the workspace Uri where the change happened. - private installChangedEmitter = new EventEmitter() + private installChangedEmitter = new EventEmitter() installChanged = this.installChangedEmitter.event - constructor(outputChannel: OutputChannel, defaultToolchain: string) { + constructor(outputChannel: OutputChannel, freshInstallDefaultToolchain: string) { this.outputChannel = outputChannel - this.defaultToolchain = defaultToolchain + this.freshInstallDefaultToolchain = freshInstallDefaultToolchain if (isRunningTest()) { this.promptUser = false if (process.env.LEAN4_PROMPT_USER === 'true') { @@ -47,79 +46,15 @@ export class LeanInstaller { return this.outputChannel } - async testLeanVersion(packageUri: ExtUri): Promise { - // see if there is a lean-toolchain file and use that version info. - let leanVersion: string | undefined = - packageUri.scheme === 'file' ? await readLeanVersion(packageUri) : undefined - - if (leanVersion === undefined) { - const hasElan = await this.hasElan() - if (!hasElan) { - // Ah, there is no elan, but what if Lean is in the PATH due to custom install? - const found = await this.checkLeanVersion(packageUri, leanVersion) - if (found.error) { - return { version: '', error: 'no elan installed' } - } - } else if (packageUri.scheme === 'file' && !(await isCoreLean4Directory(packageUri))) { - const defaultVersion = await this.getElanDefaultToolchain(packageUri) - if (!defaultVersion) { - return { version: '', error: 'no default toolchain' } - } - leanVersion = defaultVersion - } - } - - const found = await this.checkLeanVersion(packageUri, leanVersion) - if (found.error && leanVersion) { - // if we have a lean-toolchain version or a workspace override then - // use that version during the installElan process. - this.defaultToolchain = leanVersion - } - return found - } - - async handleVersionChanged(packageUri: FileUri): Promise { - const key = packageUri.toString() - if (this.versionCache.has(key)) { - this.versionCache.delete(key) - } - - if (!this.promptUser) { - await this.checkAndFire(packageUri) - return - } - - if (this.prompting) { - return - } - - const restartItem = 'Restart Lean' - const item = await this.showPrompt('Lean version changed', restartItem) - if (item === restartItem) { - await this.checkAndFire(packageUri) - } + handleVersionChanged(packageUri: FileUri) { + void this.showRestartPromptAndRestart('Lean version changed', packageUri) } isPromptVisible() { return this.prompting } - private async showPrompt(message: string, ...items: string[]): Promise { - this.prompting = true - const item = await window.showErrorMessage(message, ...items) - this.prompting = false - return item - } - - private async checkAndFire(packageUri: FileUri) { - const rc = await this.testLeanVersion(packageUri) - if (rc.version === '4') { - // it works, so restart the client! - this.installChangedEmitter.fire(packageUri) - } - } - - async handleLakeFileChanged(packageUri: FileUri): Promise { + private async showRestartPromptAndRestart(message: string, packageUri: FileUri) { if (!this.promptUser) { this.installChangedEmitter.fire(packageUri) return @@ -129,43 +64,20 @@ export class LeanInstaller { return } - const restartItem = 'Restart Lean' - const item = await this.showPrompt('Lake file configuration changed', restartItem) - if (item === restartItem) { - this.installChangedEmitter.fire(packageUri) + this.prompting = true + const finalizer = () => { + this.prompting = false } + displayErrorWithOptionalInput( + message, + 'Restart Lean', + () => this.installChangedEmitter.fire(packageUri), + finalizer, + ) } - async showInstallOptions(packageUri: ExtUri): Promise { - if (!this.promptUser) { - // no need to prompt when there is no user. - return - } - const path = toolchainPath() - - // note; we keep the LeanClient alive so that it can be restarted if the - // user changes the Lean: Executable Path. - const installItem = 'Install Lean' - let prompt = "Failed to start 'lean' language server" - if (path) { - prompt += ` from ${path}` - } - - if (shouldAutofocusOutput()) { - this.outputChannel.show(true) - } - - const item = await this.showPrompt(prompt, installItem) - if (item === installItem) { - try { - await this.installElan() - this.installChangedEmitter.fire(packageUri) - } catch (err) { - const msg = '' + err - logger.log(`[LeanInstaller] restart error ${msg}`) - this.outputChannel.appendLine(msg) - } - } + handleLakeFileChanged(packageUri: FileUri) { + void this.showRestartPromptAndRestart('Lake file configuration changed', packageUri) } private removeSuffix(version: string): string { @@ -179,78 +91,6 @@ export class LeanInstaller { return s.trim() } - async checkLeanVersion(packageUri: ExtUri, version: string | undefined): Promise { - let cmd = toolchainPath() - if (!cmd) { - cmd = 'lean' - } else { - cmd = join(cmd, 'bin', 'lean') - } - const cacheKey = packageUri.toString() - if (!version && this.versionCache.has(cacheKey)) { - const result = this.versionCache.get(cacheKey) - if (result) { - return result - } - } - - addServerEnvPaths(process.env) - - let options = ['--version'] - if (version) { - // user is requesting an explicit version! - options = ['+' + version, ...options] - } - - const result: LeanVersion = { version: '', error: undefined } - try { - // If folderPath is undefined, this will use the process environment for cwd. - // Specifically, if the extension was not opened inside of a folder, it - // looks for a global (default) installation of Lean. This way, we can support - // single file editing. - logger.log(`executeWithProgress ${cmd} ${options}`) - const cwd = packageUri.scheme === 'file' ? packageUri.fsPath : undefined - const checkingResult: ExecutionResult = await batchExecute(cmd, options, cwd, { - combined: this.outputChannel, - }) - if (checkingResult.exitCode === ExecutionExitCode.CannotLaunch) { - result.error = 'lean not found' - } else if (checkingResult.exitCode === ExecutionExitCode.ExecutionError) { - if (checkingResult.stderr.match(/error: toolchain '.*' is not installed/)) { - result.error = 'selected elan default toolchain not installed - please set a new default toolchain' - } else { - result.error = 'lean version not found' - } - } else if (checkingResult.stderr.indexOf('no default toolchain') > 0) { - result.error = 'no default toolchain' - } else { - const filterVersion = /version (\d+)\.\d+\..+/ - const match = filterVersion.exec(checkingResult.stdout) - if (!match) { - return { - version: '', - error: `lean4: '${cmd} ${options}' returned incorrect version string '${checkingResult.stdout}'.`, - } - } - const major = match[1] - result.version = major - } - } catch (err) { - const msg = '' + err - logger.log(`[LeanInstaller] check lean version error ${msg}`) - if (this.outputChannel) this.outputChannel.appendLine(msg) - result.error = err - } - if (!version) { - this.versionCache.set(cacheKey, result) - } - return result - } - - getDefaultToolchain(): string { - return this.defaultToolchain - } - async getElanDefaultToolchain(packageUri: ExtUri): Promise { if (this.elanDefaultToolchain) { return this.elanDefaultToolchain @@ -302,14 +142,18 @@ export class LeanInstaller { } } - async installElan(): Promise { - if (toolchainPath()) { - void window.showErrorMessage( - "It looks like you've modified the `lean.toolchainPath` user setting." + - 'Please clear this setting before installing elan.', - ) - return false + async autoInstall(): Promise { + logger.log('[LeanInstaller] Installing Elan ...') + await this.installElan() + logger.log('[LeanInstaller] Elan installed') + } + + async installElan(): Promise<'Success' | 'InstallationFailed' | 'PendingInstallation'> { + if (this.installing) { + displayError('Elan is already being installed.') + return 'PendingInstallation' } + this.installing = true const terminalName = 'Lean installation via elan' @@ -321,7 +165,7 @@ export class LeanInstaller { terminal.show() // We register a listener, to restart the Lean extension once elan has finished. - const result = new Promise(function (resolve, reject) { + const resultPromise = new Promise(function (resolve, reject) { window.onDidCloseTerminal(async t => { if (t === terminal) { resolve(true) @@ -335,7 +179,7 @@ export class LeanInstaller { terminal.sendText( `Start-BitsTransfer -Source "${this.leanInstallerWindows}" -Destination "elan-init.ps1"\r\n` + 'Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process\r\n' + - `$rc = .\\elan-init.ps1 -NoPrompt 1 -DefaultToolchain ${this.defaultToolchain}\r\n` + + `$rc = .\\elan-init.ps1 -NoPrompt 1 -DefaultToolchain ${this.freshInstallDefaultToolchain}\r\n` + 'Write-Host "elan-init returned [$rc]"\r\n' + 'del .\\elan-init.ps1\r\n' + 'if ($rc -ne 0) {\r\n' + @@ -344,7 +188,7 @@ export class LeanInstaller { 'exit\r\n', ) } else { - const elanArgs = `-y --default-toolchain ${this.defaultToolchain}` + const elanArgs = `-y --default-toolchain ${this.freshInstallDefaultToolchain}` const prompt = '(echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")' terminal.sendText( @@ -352,10 +196,14 @@ export class LeanInstaller { ) } - // clear any previous lean version errors. - this.versionCache.clear() - this.elanDefaultToolchain = this.defaultToolchain + const result = await resultPromise + this.elanDefaultToolchain = this.freshInstallDefaultToolchain + this.installing = false + if (!result) { + displayError('Elan installation failed. Check the terminal output for errors.') + return 'InstallationFailed' + } - return result + return 'Success' } } diff --git a/vscode-lean4/src/utils/notifs.ts b/vscode-lean4/src/utils/notifs.ts new file mode 100644 index 000000000..4b290ff4e --- /dev/null +++ b/vscode-lean4/src/utils/notifs.ts @@ -0,0 +1,150 @@ +import { MessageOptions, commands, window } from 'vscode' + +// All calls to window.show(Error|Warning|Information)... should go through functions in this file +// to prevent accidentally blocking the VS Code extension. +// Specifically, we want to enforce the following invariants: +// - Notifications without input should never block the extension +// - Notifications with optional input should never block the extension +// - Notifications that block the extension must be modal + +type Notification = ( + message: string, + options: MessageOptions, + ...items: T[] +) => Thenable + +function displayNotification(notif: Notification, message: string, finalizer?: (() => void) | undefined) { + void (async () => { + await notif(message, {}) + if (finalizer) { + finalizer() + } + })() +} + +async function displayNotificationWithInput( + notif: Notification, + message: string, + ...items: T[] +): Promise { + return await notif(message, { modal: true }, ...items) +} + +function displayNotificationWithOptionalInput( + notif: Notification, + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +) { + void (async () => { + const choice = await notif(message, {}, input) + if (choice === input) { + action() + } + if (finalizer) { + finalizer() + } + })() +} + +function displayNotificationWithOutput(notif: Notification, message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithOptionalInput( + notif, + message, + 'Show Output', + () => commands.executeCommand('lean4.troubleshooting.showOutput'), + finalizer, + ) +} + +function displayNotificationWithSetupGuide(notif: Notification, message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithOptionalInput( + notif, + message, + 'Open Setup Guide', + () => commands.executeCommand('lean4.setup.showSetupGuide'), + finalizer, + ) +} + +export function displayError(message: string, finalizer?: (() => void) | undefined) { + displayNotification(window.showErrorMessage, message, finalizer) +} + +export async function displayErrorWithInput(message: string, ...items: T[]): Promise { + return await displayNotificationWithInput(window.showErrorMessage, message, ...items) +} + +export function displayErrorWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +) { + displayNotificationWithOptionalInput(window.showErrorMessage, message, input, action, finalizer) +} + +export function displayErrorWithOutput(message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithOutput(window.showErrorMessage, message, finalizer) +} + +export function displayErrorWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithSetupGuide(window.showErrorMessage, message, finalizer) +} + +export function displayWarning(message: string, finalizer?: (() => void) | undefined) { + displayNotification(window.showWarningMessage, message, finalizer) +} + +export async function displayWarningWithInput( + message: string, + ...items: T[] +): Promise { + return await displayNotificationWithInput(window.showWarningMessage, message, ...items) +} + +export function displayWarningWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +) { + displayNotificationWithOptionalInput(window.showWarningMessage, message, input, action, finalizer) +} + +export function displayWarningWithOutput(message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithOutput(window.showWarningMessage, message, finalizer) +} + +export function displayWarningWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithSetupGuide(window.showWarningMessage, message, finalizer) +} + +export function displayInformation(message: string, finalizer?: (() => void) | undefined) { + displayNotification(window.showInformationMessage, message, finalizer) +} + +export async function displayInformationWithInput( + message: string, + ...items: T[] +): Promise { + return await displayNotificationWithInput(window.showInformationMessage, message, ...items) +} + +export function displayInformationWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +) { + displayNotificationWithOptionalInput(window.showInformationMessage, message, input, action, finalizer) +} + +export function displayInformationWithOutput(message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithOutput(window.showInformationMessage, message, finalizer) +} + +export function displayInformationWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { + displayNotificationWithSetupGuide(window.showInformationMessage, message, finalizer) +} diff --git a/vscode-lean4/src/utils/pathExtensionProvider.ts b/vscode-lean4/src/utils/pathExtensionProvider.ts new file mode 100644 index 000000000..e4662f7c0 --- /dev/null +++ b/vscode-lean4/src/utils/pathExtensionProvider.ts @@ -0,0 +1,37 @@ +import { Disposable, workspace } from 'vscode' +import { envPathExtensions } from '../config' +import { PATH, setProcessEnvPATH } from './envPath' + +export class PathExtensionProvider implements Disposable { + currentPathExtensions: PATH = PATH.empty() + subscriptions: Disposable[] = [] + + private constructor() { + this.replaceEnvPathExtensionsInPATH() + this.subscriptions.push( + workspace.onDidChangeConfiguration(e => { + if (e.affectsConfiguration('lean4.envPathExtensions')) { + this.replaceEnvPathExtensionsInPATH() + } + }), + ) + } + + static withAddedEnvPathExtensions(): PathExtensionProvider { + return new PathExtensionProvider() + } + + replaceEnvPathExtensionsInPATH() { + const previousPathExtensions = this.currentPathExtensions + this.currentPathExtensions = envPathExtensions() + const path = PATH.ofProcessEnv() + const originalPath = path.filter(path => !previousPathExtensions.includes(path)) + setProcessEnvPATH(this.currentPathExtensions.join(originalPath)) + } + + dispose() { + for (const s of this.subscriptions) { + s.dispose() + } + } +} diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts index ec43856b2..77de0382e 100644 --- a/vscode-lean4/src/utils/projectInfo.ts +++ b/vscode-lean4/src/utils/projectInfo.ts @@ -1,7 +1,6 @@ import * as fs from 'fs' import { FileUri, getWorkspaceFolderUri } from './exturi' import { fileExists } from './fsHelper' -import { logger } from './logger' import path = require('path') // Detect lean4 root directory (works for both lean4 repo and nightly distribution) @@ -31,7 +30,7 @@ export async function isCoreLean4Directory(path: FileUri): Promise { } // Find the root of a Lean project and the Uri for the 'lean-toolchain' file found there. -export async function findLeanPackageRoot(uri: FileUri): Promise<[FileUri, FileUri | undefined]> { +export async function findLeanProjectRootInfo(uri: FileUri): Promise<[FileUri, FileUri | undefined]> { const toolchainFileName = 'lean-toolchain' let path = uri @@ -78,37 +77,35 @@ export async function findLeanPackageRoot(uri: FileUri): Promise<[FileUri, FileU return [bestFolder, bestLeanToolchain] } -// Find the lean project root for the given document and return the -// Uri for the project root and the "version" information contained -// in any 'lean-toolchain' file found there. -export async function findLeanPackageVersionInfo(uri: FileUri): Promise<[FileUri, string | undefined]> { - const [packageUri, packageFileUri] = await findLeanPackageRoot(uri) - - let version: string | undefined - if (packageFileUri) { - try { - version = await readLeanVersionFile(packageFileUri) - } catch (err) { - logger.log(`findLeanPackageVersionInfo caught exception ${err}`) - } +export async function findLeanProjectRoot(uri: FileUri): Promise { + const [projectRootUri, _] = await findLeanProjectRootInfo(uri) + return projectRootUri +} + +export async function findLeanProjectInfo(uri: FileUri): Promise<[FileUri, string | undefined]> { + const [projectUri, toolchainUri] = await findLeanProjectRootInfo(uri) + if (!toolchainUri) { + return [projectUri, undefined] } - return [packageUri, version] + return [projectUri, await readLeanToolchainFile(toolchainUri)] } -// Find the 'lean-toolchain' in the given package root and -// extract the Lean version info from it. -export async function readLeanVersion(packageUri: FileUri): Promise { +export async function readLeanToolchain(projectUri: FileUri): Promise { const toolchainFileName = 'lean-toolchain' - const leanToolchain = packageUri.join(toolchainFileName) - if (fs.existsSync(leanToolchain.fsPath)) { - return await readLeanVersionFile(leanToolchain) + const leanToolchain = projectUri.join(toolchainFileName) + if (!fs.existsSync(leanToolchain.fsPath)) { + return undefined } - return undefined + return await readLeanToolchainFile(leanToolchain) } -async function readLeanVersionFile(packageFileUri: FileUri): Promise { - return (await fs.promises.readFile(packageFileUri.fsPath, { encoding: 'utf-8' })).trim() +async function readLeanToolchainFile(toolchainFileUri: FileUri): Promise { + try { + return (await fs.promises.readFile(toolchainFileUri.fsPath, { encoding: 'utf-8' })).trim() + } catch { + return undefined + } } export async function isValidLeanProject(projectFolder: FileUri): Promise { diff --git a/vscode-lean4/src/utils/setupDiagnostics.ts b/vscode-lean4/src/utils/setupDiagnostics.ts index 2f33aaed3..3812c4496 100644 --- a/vscode-lean4/src/utils/setupDiagnostics.ts +++ b/vscode-lean4/src/utils/setupDiagnostics.ts @@ -1,41 +1,498 @@ -import { OutputChannel } from 'vscode' -import { batchExecute, ExecutionExitCode, ExecutionResult } from './batch' -import { FileUri } from './exturi' +import * as os from 'os' +import { SemVer } from 'semver' +import { Disposable, OutputChannel, TextDocument, commands, env, window, workspace } from 'vscode' +import { shouldShowSetupWarnings } from '../config' +import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress } from './batch' +import { ExtUri, FileUri, extUriEquals, toExtUri } from './exturi' +import { + displayError, + displayErrorWithInput, + displayErrorWithOptionalInput, + displayErrorWithOutput, + displayErrorWithSetupGuide, + displayInformationWithInput, + displayWarning, + displayWarningWithInput, + displayWarningWithOptionalInput, + displayWarningWithOutput, + displayWarningWithSetupGuide, +} from './notifs' +import { checkParentFoldersForLeanProject, findLeanProjectRoot, isValidLeanProject } from './projectInfo' + +export type SystemQueryResult = { + operatingSystem: string + cpuArchitecture: string + cpuModels: string + totalMemory: string +} + +export type VersionQueryResult = + | { kind: 'Success'; version: SemVer } + | { kind: 'CommandNotFound' } + | { kind: 'CommandError'; message: string } + | { kind: 'InvalidVersion'; versionResult: string } + +const recommendedElanVersion = new SemVer('3.1.1') + +export type ElanVersionDiagnosis = + | { kind: 'UpToDate'; version: SemVer } + | { kind: 'Outdated'; currentVersion: SemVer; recommendedVersion: SemVer } + | { kind: 'NotInstalled' } + | { kind: 'ExecutionError'; message: string } + +export type ProjectSetupDiagnosis = + | { kind: 'SingleFile' } + | { kind: 'MissingLeanToolchain'; folder: FileUri; parentProjectFolder: FileUri | undefined } + | { kind: 'ValidProjectSetup'; projectFolder: FileUri } + +export type LeanVersionDiagnosis = + | { kind: 'UpToDate'; version: SemVer } + | { kind: 'IsLean3Version'; version: SemVer } + | { kind: 'IsAncientLean4Version'; version: SemVer } + | { kind: 'NotInstalled' } + | { kind: 'ExecutionError'; message: string } + +export enum PreconditionCheckResult { + Fulfilled = 0, + Warning = 1, + Fatal = 2, +} + +export function worstPreconditionViolation( + a: PreconditionCheckResult, + b: PreconditionCheckResult, +): PreconditionCheckResult { + return Math.max(a, b) +} + +export function versionQueryResult(executionResult: ExecutionResult, versionRegex: RegExp): VersionQueryResult { + if (executionResult.exitCode === ExecutionExitCode.CannotLaunch) { + return { kind: 'CommandNotFound' } + } + + if (executionResult.exitCode === ExecutionExitCode.ExecutionError) { + return { kind: 'CommandError', message: executionResult.combined } + } + + const match = versionRegex.exec(executionResult.stdout) + if (!match) { + return { kind: 'InvalidVersion', versionResult: executionResult.stdout } + } + + return { kind: 'Success', version: new SemVer(match[1]) } +} + +export function checkElanVersion(elanVersionResult: VersionQueryResult): ElanVersionDiagnosis { + switch (elanVersionResult.kind) { + case 'CommandNotFound': + return { kind: 'NotInstalled' } + + case 'CommandError': + return { kind: 'ExecutionError', message: elanVersionResult.message } + + case 'InvalidVersion': + return { + kind: 'ExecutionError', + message: `Invalid Elan version format: '${elanVersionResult.versionResult}'`, + } + + case 'Success': + if (elanVersionResult.version.compare(recommendedElanVersion) < 0) { + return { + kind: 'Outdated', + currentVersion: elanVersionResult.version, + recommendedVersion: recommendedElanVersion, + } + } + return { kind: 'UpToDate', version: elanVersionResult.version } + } +} + +export function checkLeanVersion(leanVersionResult: VersionQueryResult): LeanVersionDiagnosis { + if (leanVersionResult.kind === 'CommandNotFound') { + return { kind: 'NotInstalled' } + } + + if (leanVersionResult.kind === 'CommandError') { + return { + kind: 'ExecutionError', + message: leanVersionResult.message, + } + } + + if (leanVersionResult.kind === 'InvalidVersion') { + return { + kind: 'ExecutionError', + message: `Invalid Lean version format: '${leanVersionResult.versionResult}'`, + } + } + + const leanVersion = leanVersionResult.version + if (leanVersion.major === 3) { + return { kind: 'IsLean3Version', version: leanVersion } + } + + if (leanVersion.major === 4 && leanVersion.minor === 0 && leanVersion.prerelease.length > 0) { + return { kind: 'IsAncientLean4Version', version: leanVersion } + } + + return { kind: 'UpToDate', version: leanVersion } +} export class SetupDiagnoser { - channel: OutputChannel - cwdUri: FileUri | undefined + readonly channel: OutputChannel + readonly cwdUri: FileUri | undefined constructor(channel: OutputChannel, cwdUri: FileUri | undefined) { this.channel = channel this.cwdUri = cwdUri } - async checkLakeAndDepsAvailable(): Promise<'Success' | 'LakeUnavailable' | 'GitUnavailable'> { - if (!(await this.checkLakeAvailable())) { - return 'LakeUnavailable' + async checkCurlAvailable(): Promise { + const curlVersionResult = await this.runSilently('curl', ['--version']) + return curlVersionResult.exitCode === ExecutionExitCode.Success + } + + async checkGitAvailable(): Promise { + const gitVersionResult = await this.runSilently('git', ['--version']) + return gitVersionResult.exitCode === ExecutionExitCode.Success + } + + async queryLakeVersion(): Promise { + const lakeVersionResult = await this.runWithProgress('lake', ['--version'], 'Checking Lake version') + return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) + } + + async checkLakeAvailable(): Promise { + const lakeVersionResult = await this.queryLakeVersion() + return lakeVersionResult.kind === 'Success' + } + + querySystemInformation(): SystemQueryResult { + const cpuModels = os.cpus().map(cpu => cpu.model) + const groupedCpuModels = new Map() + for (const cpuModel of cpuModels) { + const counter: number | undefined = groupedCpuModels.get(cpuModel) + if (counter === undefined) { + groupedCpuModels.set(cpuModel, 1) + } else { + groupedCpuModels.set(cpuModel, counter + 1) + } } - if (!(await this.checkGitAvailable())) { - return 'GitUnavailable' + const formattedCpuModels = Array.from(groupedCpuModels.entries()) + .map(([cpuModel, amount]) => `${amount} x ${cpuModel}`) + .join(', ') + + const totalMemory = (os.totalmem() / 1_000_000_000).toFixed(2) + + return { + operatingSystem: `${os.type()} (release: ${os.release()})`, + cpuArchitecture: os.arch(), + cpuModels: formattedCpuModels, + totalMemory: `${totalMemory} GB`, } - return 'Success' } - async checkLakeAvailable(): Promise { - const lakeVersionResult = await this.runSilently('lake', ['--version']) - return lakeVersionResult.exitCode === ExecutionExitCode.Success + async queryLeanVersion(): Promise { + const leanVersionResult = await this.runWithProgress('lean', ['--version'], 'Checking Lean version') + return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) } - async checkGitAvailable(): Promise { - const gitVersionResult = await batchExecute('git', ['--version']) - return gitVersionResult.exitCode === ExecutionExitCode.Success + async queryElanVersion(): Promise { + const elanVersionResult = await this.runSilently('elan', ['--version']) + return versionQueryResult(elanVersionResult, /elan (\d+\.\d+\.\d+)/) + } + + async queryElanShow(): Promise { + return await this.runSilently('elan', ['show']) + } + + async elanVersion(): Promise { + const elanVersionResult = await this.queryElanVersion() + return checkElanVersion(elanVersionResult) + } + + async projectSetup(): Promise { + if (this.cwdUri === undefined) { + return { kind: 'SingleFile' } + } + + if (!(await isValidLeanProject(this.cwdUri))) { + const parentProjectFolder: FileUri | undefined = await checkParentFoldersForLeanProject(this.cwdUri) + return { kind: 'MissingLeanToolchain', folder: this.cwdUri, parentProjectFolder } + } + + return { kind: 'ValidProjectSetup', projectFolder: this.cwdUri } + } + + async projectLeanVersion(): Promise { + const leanVersionResult = await this.queryLeanVersion() + return checkLeanVersion(leanVersionResult) } private async runSilently(executablePath: string, args: string[]): Promise { return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel }) } + + private async runWithProgress(executablePath: string, args: string[], title: string): Promise { + return batchExecuteWithProgress(executablePath, args, title, { + cwd: this.cwdUri?.fsPath, + channel: this.channel, + }) + } } export function diagnose(channel: OutputChannel, cwdUri: FileUri | undefined): SetupDiagnoser { return new SetupDiagnoser(channel, cwdUri) } + +export type FullDiagnostics = { + systemInfo: SystemQueryResult + isCurlAvailable: boolean + isGitAvailable: boolean + elanVersionDiagnosis: ElanVersionDiagnosis + leanVersionDiagnosis: LeanVersionDiagnosis + projectSetupDiagnosis: ProjectSetupDiagnosis + elanShowOutput: ExecutionResult +} + +function formatCommandOutput(cmdOutput: string): string { + return '\n```\n' + cmdOutput + '\n```' +} + +function formatElanVersionDiagnosis(d: ElanVersionDiagnosis): string { + switch (d.kind) { + case 'UpToDate': + return `Reasonably up-to-date (version: ${d.version.toString()})` + case 'Outdated': + return `Outdated (version: ${d.currentVersion.toString()}, recommended version: ${d.recommendedVersion.toString()})` + case 'ExecutionError': + return 'Execution error: ' + formatCommandOutput(d.message) + case 'NotInstalled': + return 'Not installed' + } +} + +function formatLeanVersionDiagnosis(d: LeanVersionDiagnosis): string { + switch (d.kind) { + case 'UpToDate': + return `Reasonably up-to-date (version: ${d.version})` + case 'IsLean3Version': + return `Lean 3 version (version: ${d.version})` + case 'IsAncientLean4Version': + return `Pre-stable-release Lean 4 version (version: ${d.version})` + case 'ExecutionError': + return 'Execution error: ' + formatCommandOutput(d.message) + case 'NotInstalled': + return 'Not installed' + } +} + +function formatProjectSetupDiagnosis(d: ProjectSetupDiagnosis): string { + switch (d.kind) { + case 'SingleFile': + return 'No open project' + case 'MissingLeanToolchain': + const parentProjectFolder = + d.parentProjectFolder === undefined + ? '' + : `(Valid Lean project in parent folder: ${d.parentProjectFolder.fsPath})` + return `Folder without lean-toolchain file (no valid Lean project) (path: ${d.folder.fsPath}) ${parentProjectFolder}` + case 'ValidProjectSetup': + return `Valid Lean project (path: ${d.projectFolder.fsPath})` + } +} + +function formatElanShowOutput(r: ExecutionResult): string { + if (r.exitCode === ExecutionExitCode.CannotLaunch) { + return 'Elan not installed' + } + if (r.exitCode === ExecutionExitCode.ExecutionError) { + return 'Execution error: ' + formatCommandOutput(r.combined) + } + return formatCommandOutput(r.stdout) +} + +export function formatFullDiagnostics(d: FullDiagnostics): string { + return [ + `**Operating system**: ${d.systemInfo.operatingSystem}`, + `**CPU architecture**: ${d.systemInfo.cpuArchitecture}`, + `**CPU model**: ${d.systemInfo.cpuModels}`, + `**Available RAM**: ${d.systemInfo.totalMemory}`, + '', + `**Curl installed**: ${d.isCurlAvailable}`, + `**Git installed**: ${d.isGitAvailable}`, + `**Elan**: ${formatElanVersionDiagnosis(d.elanVersionDiagnosis)}`, + `**Lean**: ${formatLeanVersionDiagnosis(d.leanVersionDiagnosis)}`, + `**Project**: ${formatProjectSetupDiagnosis(d.projectSetupDiagnosis)}`, + '', + '-------------------------------------', + '', + `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`, + ].join('\n') +} + +export async function performFullDiagnosis( + channel: OutputChannel, + cwdUri: FileUri | undefined, +): Promise { + const diagnose = new SetupDiagnoser(channel, cwdUri) + return { + systemInfo: diagnose.querySystemInformation(), + isCurlAvailable: await diagnose.checkCurlAvailable(), + isGitAvailable: await diagnose.checkGitAvailable(), + elanVersionDiagnosis: await diagnose.elanVersion(), + leanVersionDiagnosis: await diagnose.projectLeanVersion(), + projectSetupDiagnosis: await diagnose.projectSetup(), + elanShowOutput: await diagnose.queryElanShow(), + } +} + +export class FullDiagnosticsProvider implements Disposable { + private subscriptions: Disposable[] = [] + private outputChannel: OutputChannel + // Under normal circumstances, we would use the last active `LeanClient` from `LeanClientProvider.getActiveClient()` + // to determine the document that the user is currently working on. + // However, when providing setup diagnostics, there might not be an active client due to errors in the user's setup, + // in which case we still want to provide adequate diagnostics. Hence, we track the last active lean document + // separately, regardless of whether there is an actual `LeanClient` managing it. + private lastActiveLeanDocumentUri: ExtUri | undefined + + constructor(outputChannel: OutputChannel) { + this.outputChannel = outputChannel + + if (window.activeTextEditor !== undefined) { + this.lastActiveLeanDocumentUri = FullDiagnosticsProvider.getLean4DocUri(window.activeTextEditor.document) + } + + window.onDidChangeActiveTextEditor(e => { + if (e === undefined) { + return + } + const docUri = FullDiagnosticsProvider.getLean4DocUri(e.document) + if (docUri === undefined) { + return + } + + this.lastActiveLeanDocumentUri = docUri + }, this.subscriptions) + workspace.onDidCloseTextDocument(doc => { + if (this.lastActiveLeanDocumentUri === undefined) { + return + } + + const docUri = FullDiagnosticsProvider.getLean4DocUri(doc) + if (docUri === undefined) { + return + } + + if (extUriEquals(docUri, this.lastActiveLeanDocumentUri)) { + this.lastActiveLeanDocumentUri = undefined + } + }, this.subscriptions) + + this.subscriptions.push( + commands.registerCommand('lean4.troubleshooting.showSetupInformation', () => + this.performAndDisplayFullDiagnosis(), + ), + ) + } + + async performAndDisplayFullDiagnosis() { + const projectUri = + this.lastActiveLeanDocumentUri !== undefined && this.lastActiveLeanDocumentUri.scheme === 'file' + ? await findLeanProjectRoot(this.lastActiveLeanDocumentUri) + : undefined + const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri) + const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics) + const copyToClipboardInput = 'Copy to Clipboard' + const choice = await displayInformationWithInput(formattedFullDiagnostics, copyToClipboardInput) + if (choice === copyToClipboardInput) { + await env.clipboard.writeText(formattedFullDiagnostics) + } + } + + private static getLean4DocUri(doc: TextDocument): ExtUri | undefined { + if (doc.languageId !== 'lean4') { + return undefined + } + return toExtUri(doc.uri) + } + + dispose() { + for (const s of this.subscriptions) { + s.dispose() + } + } +} + +export function displaySetupError(message: string, finalizer?: (() => void) | undefined) { + displayError(message, finalizer) +} + +export async function displaySetupErrorWithInput( + message: string, + ...items: T[] +): Promise { + return await displayErrorWithInput(message, ...items) +} + +export function displaySetupErrorWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +) { + displayErrorWithOptionalInput(message, input, action, finalizer) +} + +export function displaySetupErrorWithOutput(message: string, finalizer?: (() => void) | undefined) { + displayErrorWithOutput(message, finalizer) +} + +export function displaySetupErrorWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { + displayErrorWithSetupGuide(message, finalizer) +} + +export function displaySetupWarning(message: string, finalizer?: (() => void) | undefined) { + if (!shouldShowSetupWarnings()) { + return + } + displayWarning(message, finalizer) +} + +export async function displaySetupWarningWithInput( + message: string, + ...items: T[] +): Promise { + if (!shouldShowSetupWarnings()) { + return undefined + } + return await displayWarningWithInput(message, ...items) +} + +export function displaySetupWarningWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +) { + if (!shouldShowSetupWarnings()) { + return + } + displayWarningWithOptionalInput(message, input, action, finalizer) +} + +export function displaySetupWarningWithOutput(message: string, finalizer?: (() => void) | undefined) { + if (!shouldShowSetupWarnings()) { + return + } + displayWarningWithOutput(message, finalizer) +} + +export function displaySetupWarningWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { + if (!shouldShowSetupWarnings()) { + return + } + displayWarningWithSetupGuide(message, finalizer) +} diff --git a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts index cbe4bfd6a..19c520447 100644 --- a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts +++ b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts @@ -1,7 +1,7 @@ import * as assert from 'assert' import { suite } from 'mocha' -import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' +import { displayInformation } from '../../../src/utils/notifs' import { cleanTempFolder, closeAllEditors, @@ -16,21 +16,21 @@ import { suite('Lean4 Bootstrap Test Suite', () => { test('Install elan on demand', async () => { logger.log('=================== Install elan on demand ===================') - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) cleanTempFolder('elan') // this will wait up to 60 seconds to do full elan lean install, so test machines better // be able to do that. - const lean = await initLean4Untitled('#eval Lean.versionString') - const info = lean.exports.infoProvider + const features = await initLean4Untitled('#eval Lean.versionString') + const info = features.infoProvider const expected = '4.0.0-nightly-' assert(info, 'No InfoProvider export') // give it a extra long timeout in case test machine is really slow. logger.log('Wait for elan install of Lean nightly build...') - await waitForActiveClient(lean.exports.clientProvider, 120) - await waitForActiveClientRunning(lean.exports.clientProvider, 300) + await waitForActiveClient(features.clientProvider, 120) + await waitForActiveClientRunning(features.clientProvider, 300) const hackNeeded = false if (hackNeeded) { @@ -66,11 +66,11 @@ suite('Lean4 Bootstrap Test Suite', () => { ) logger.log(`=================== Install leanprover/lean4:${version} build on demand ===================`) - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) // Lean is already installed so this should be quick. - const lean = await initLean4Untitled('#eval Lean.versionString') - const info = lean.exports.infoProvider + const features = await initLean4Untitled('#eval Lean.versionString') + const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('Wait for Lean nightly build server to start...') diff --git a/vscode-lean4/test/suite/docview/docview.test.ts b/vscode-lean4/test/suite/docview/docview.test.ts index 5d3f29d28..e7440687c 100644 --- a/vscode-lean4/test/suite/docview/docview.test.ts +++ b/vscode-lean4/test/suite/docview/docview.test.ts @@ -4,6 +4,7 @@ import * as path from 'path' import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' +import { displayInformation } from '../../../src/utils/notifs' import { closeAllEditors, extractPhrase, @@ -23,11 +24,11 @@ suite('Documentation View Test Suite', () => { // This test opens the documentation view and selects the "Example" link. logger.log('=================== Documentation View Example Test ===================') - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') const mainFile = path.join(testsRoot, 'Main.lean') - const lean = await initLean4(mainFile) - const info = lean.exports.infoProvider + const features = await initLean4(mainFile) + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedVersion = 'Hello:' let html = await waitForInfoviewHtml(info, expectedVersion) @@ -36,7 +37,7 @@ suite('Documentation View Test Suite', () => { await vscode.commands.executeCommand('lean4.docView.open') - const docView = lean.exports.docView + const docView = features.docView assert(docView, 'No docView export') const expectedMenuItem = 'Abbreviations Cheatsheet' html = await waitForDocViewHtml(docView, expectedMenuItem) diff --git a/vscode-lean4/test/suite/index/index.ts b/vscode-lean4/test/suite/index/index.ts index 48eef0b13..e72561b63 100644 --- a/vscode-lean4/test/suite/index/index.ts +++ b/vscode-lean4/test/suite/index/index.ts @@ -1,7 +1,7 @@ import * as glob from 'glob' import * as Mocha from 'mocha' import * as path from 'path' -import { getTestFolder, isElanDisabled } from '../../../src/config' +import { getTestFolder } from '../../../src/config' import { logger } from '../../../src/utils/logger' export function run(testsRoot: string, cb: (error: any, failures?: number) => void): void { @@ -21,10 +21,6 @@ export function run(testsRoot: string, cb: (error: any, failures?: number) => vo logger.log('>>>>>>>>> testsRoot=' + testsRoot) - if (isElanDisabled()) { - logger.log('>>>>>>>>> running without elan') - } - glob('**/**.test.js', { cwd: testsRoot }, (err, files) => { if (err) { return cb(err) diff --git a/vscode-lean4/test/suite/info/info.test.ts b/vscode-lean4/test/suite/info/info.test.ts index c27d0cb39..72f0df9e7 100644 --- a/vscode-lean4/test/suite/info/info.test.ts +++ b/vscode-lean4/test/suite/info/info.test.ts @@ -24,8 +24,8 @@ suite('InfoView Test Suite', () => { const b = 22 const expectedEval1 = (a * b).toString() - const lean = await initLean4Untitled(`#eval ${a}*${b}`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval ${a}*${b}`) + const info = features.infoProvider assert(info, 'No InfoProvider export') await assertStringInInfoview(info, expectedEval1) @@ -49,8 +49,8 @@ suite('InfoView Test Suite', () => { const c = 77 const d = 7 - const lean = await initLean4Untitled(`#eval ${a}*${b}`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval ${a}*${b}`) + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedEval1 = (a * b).toString() @@ -84,12 +84,12 @@ suite('InfoView Test Suite', () => { const expectedEval = '[1, 2, 3]' - const lean = await initLean4Untitled('#eval [1, 1+1, 1+1+1] \n') + const features = await initLean4Untitled('#eval [1, 1+1, 1+1+1] \n') const editor = await waitForActiveEditor() const firstLine = editor.document.lineAt(0).range editor.selection = new vscode.Selection(firstLine.end, firstLine.end) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') await waitForInfoviewHtml(info, expectedEval, 30, 1000, false) @@ -127,8 +127,8 @@ suite('InfoView Test Suite', () => { const b = 95 const prefix = 'Lean version is:' - const lean = await initLean4Untitled(`#eval ${a}*${b}`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval ${a}*${b}`) + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedEval = (a * b).toString() diff --git a/vscode-lean4/test/suite/lean3/lean3.test.ts b/vscode-lean4/test/suite/lean3/lean3.test.ts index e46b746f9..d5a3ae251 100644 --- a/vscode-lean4/test/suite/lean3/lean3.test.ts +++ b/vscode-lean4/test/suite/lean3/lean3.test.ts @@ -3,11 +3,17 @@ import { suite } from 'mocha' import * as path from 'path' import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' -import { closeAllEditors, waitForActiveEditor, waitForActiveExtension } from '../utils/helpers' +import { displayInformation } from '../../../src/utils/notifs' +import { + assertLean4FeaturesNotLoaded, + closeAllEditors, + waitForActiveEditor, + waitForActiveExtension, +} from '../utils/helpers' suite('Lean3 Compatibility Test Suite', () => { test('Lean3 project', async () => { - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'lean3') @@ -21,7 +27,7 @@ suite('Lean3 Compatibility Test Suite', () => { const lean = await waitForActiveExtension('leanprover.lean4') assert(lean, 'Lean extension not loaded') - assert(!lean.exports.isLean4Project, 'Lean4 extension should not be running!') + await assertLean4FeaturesNotLoaded(lean.exports) logger.log('Checking vscode commands...') const cmds = await vscode.commands.getCommands(true) diff --git a/vscode-lean4/test/suite/multi/multi.test.ts b/vscode-lean4/test/suite/multi/multi.test.ts index 3c34bac53..4e9e9946e 100644 --- a/vscode-lean4/test/suite/multi/multi.test.ts +++ b/vscode-lean4/test/suite/multi/multi.test.ts @@ -3,6 +3,7 @@ import { suite } from 'mocha' import * as path from 'path' import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' +import { displayInformation } from '../../../src/utils/notifs' import { assertStringInInfoview, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers' suite('Multi-Folder Test Suite', () => { @@ -10,13 +11,13 @@ suite('Multi-Folder Test Suite', () => { logger.log('=================== Load Lean Files in a multi-project workspace ===================') // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) const multiRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'multi') - const lean = await initLean4(path.join(multiRoot, 'test', 'Main.lean')) + const features = await initLean4(path.join(multiRoot, 'test', 'Main.lean')) // verify we have a nightly build running in this folder. - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') await assertStringInInfoview(info, '4.0.0-nightly-') @@ -30,7 +31,7 @@ suite('Multi-Folder Test Suite', () => { await assertStringInInfoview(info, version) // Now verify we have 2 LeanClients running. - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') const actual = clients.getClients().length assert(actual === 2, 'Expected 2 LeanClients to be running, but found ' + actual) diff --git a/vscode-lean4/test/suite/pre-bootstrap/user.test.ts b/vscode-lean4/test/suite/pre-bootstrap/user.test.ts deleted file mode 100644 index 53993bdae..000000000 --- a/vscode-lean4/test/suite/pre-bootstrap/user.test.ts +++ /dev/null @@ -1,56 +0,0 @@ -import * as assert from 'assert' -import { suite } from 'mocha' -import * as path from 'path' -import * as vscode from 'vscode' -import { logger } from '../../../src/utils/logger' -import { cleanTempFolder, closeAllEditors, initLean4, waitForInfoviewLambda } from '../utils/helpers' - -suite('Lean4 Pre-bootstrap Test Suite', () => { - test('Test user sees the install prompt', async () => { - logger.log('=================== Test user sees the install prompt ===================') - void vscode.window.showInformationMessage('Running tests: ' + __dirname) - - cleanTempFolder('elan') - - // this will wait up to 60 seconds to do full elan lean install, so test machines better - // be able to do that. - const promptUser = true - const projectRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') - const lean = await initLean4(path.join(projectRoot, 'Main.lean')) - const info = lean.exports.infoProvider - const expected1 = 'Waiting for Lean server to start...' - const expected2 = 'nightly' // lean was already installed before this test started! - assert(info, 'No InfoProvider export') - - // give it a extra long timeout in case test machine is really slow. - logger.log(expected1) - - const lambda = (s: string) => { - return s.indexOf(expected1) > 0 || s.indexOf(expected2) > 0 - } - - let html = await waitForInfoviewLambda(info, lambda, 60) - - let retries = 10 - while (html.indexOf(expected1) > 0) { - const installer = lean.exports.installer - if (!installer?.isPromptVisible()) { - html = await waitForInfoviewLambda(info, lambda, 10) - retries-- - if (retries === 0) { - logger.log('>>> infoview contains:') - logger.log(html) - logger.log('>>> end of infoview contents') - assert.fail('Infoview is in a weird state') - } - logger.log('Continuing...') - } else { - logger.log('Great, it is prompting the user!') - break // great, it is prompting the user - } - } - - // make sure test is always run in predictable state, which is no file or folder open - await closeAllEditors() - }).timeout(600000) // give it 5 minutes to install lean in case test machine is really slow. -}) diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts index 634b66553..c44d5cd28 100644 --- a/vscode-lean4/test/suite/restarts/restarts.test.ts +++ b/vscode-lean4/test/suite/restarts/restarts.test.ts @@ -4,6 +4,7 @@ import * as path from 'path' import * as vscode from 'vscode' import { FileUri } from '../../../src/utils/exturi' import { logger } from '../../../src/utils/logger' +import { displayInformation } from '../../../src/utils/notifs' import { assertStringInInfoview, closeAllEditors, @@ -24,18 +25,18 @@ suite('Lean Server Restart Test Suite', () => { logger.log( '=================== Test worker crashed and client running - Restarting Lean Server ===================', ) - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) // add normal values to initialize lean4 file const hello = 'Hello World' - const lean = await initLean4Untitled(`#eval "${hello}"`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval "${hello}"`) + const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('make sure language server is up and running.') await assertStringInInfoview(info, hello) - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') logger.log('Insert eval that causes crash.') @@ -69,18 +70,18 @@ suite('Lean Server Restart Test Suite', () => { logger.log( '=================== Test worker crashed and client running (Refreshing dependencies) ===================', ) - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) // add normal values to initialize lean4 file const hello = 'Hello World' - const lean = await initLean4Untitled(`#eval "${hello}"`) - const info = lean.exports.infoProvider + const features = await initLean4Untitled(`#eval "${hello}"`) + const info = features.infoProvider assert(info, 'No InfoProvider export') logger.log('make sure language server is up and running.') await assertStringInInfoview(info, hello) - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') logger.log('Insert eval that causes crash.') @@ -112,16 +113,16 @@ suite('Lean Server Restart Test Suite', () => { test('Restart Server', async () => { logger.log('=================== Test Restart Server ===================') - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) // Test we can restart the lean server const simpleRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') // run this code twice to ensure that it still works after a Restart Server for (let i = 0; i < 2; i++) { - const lean = await initLean4(path.join(simpleRoot, 'Main.lean')) + const features = await initLean4(path.join(simpleRoot, 'Main.lean')) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') const activeEditor = vscode.window.activeTextEditor @@ -139,7 +140,7 @@ suite('Lean Server Restart Test Suite', () => { logger.log(`>>> Found "${versionString}" in infoview`) logger.log('Now invoke the restart server command') - const clients = lean.exports.clientProvider + const clients = features.clientProvider assert(clients, 'No LeanClientProvider export') const client = clients.getClientForFolder(new FileUri(simpleRoot)) if (client) { diff --git a/vscode-lean4/test/suite/runTest.ts b/vscode-lean4/test/suite/runTest.ts index 41a210470..57a5dc16d 100644 --- a/vscode-lean4/test/suite/runTest.ts +++ b/vscode-lean4/test/suite/runTest.ts @@ -52,19 +52,6 @@ async function main() { clearUserWorkspaceData(vscodeTestPath) - // run pre-bootstrap tests on a lean project that has a lean-toolchain (bug #265) - await runTests({ - vscodeExecutablePath, - extensionDevelopmentPath, - extensionTestsPath: path.resolve(__dirname, 'index'), - extensionTestsEnv: { - LEAN4_TEST_FOLDER: 'pre-bootstrap', - DEFAULT_LEAN_TOOLCHAIN: test_version, - LEAN4_PROMPT_USER: 'true', - }, - launchArgs: ['--new-window', '--disable-gpu'], - }) - // The '--new-window' doesn't see to be working, so this hack // ensures the following test does not re-open the previous folder clearUserWorkspaceData(vscodeTestPath) @@ -83,26 +70,6 @@ async function main() { // now that elan is installed we can run the lean3 test in one vs code instance, // using `open folder` since lean3 doesn't like ad-hoc files. - // BUGBUG: this test has begun to fail on newer vscode builds with "Uncaught Error: write EPIPE" - // await runTests({ - // vscodeExecutablePath, - // extensionDevelopmentPath, - // extensionTestsPath: path.resolve(__dirname, 'index'), - // extensionTestsEnv: {'LEAN4_TEST_FOLDER': 'lean3'}, - // launchArgs: ['--new-window', '--disable-gpu'] }); - // // The '--new-window' doesn't see to be working, so this hack - // // ensures the following test does not re-open the lean3 folder - // clearUserWorkspaceData(vscodeTestPath); - - // run 'no elan' tests - await runTests({ - vscodeExecutablePath, - extensionDevelopmentPath, - extensionTestsPath: path.resolve(__dirname, 'index'), - extensionTestsEnv: { LEAN4_TEST_FOLDER: 'simple', DISABLE_ELAN: '1', DEFAULT_LEAN_TOOLCHAIN: test_version }, - launchArgs: ['--new-window', '--disable-gpu'], - }) - clearUserWorkspaceData(vscodeTestPath) // run the infoView tests @@ -110,7 +77,7 @@ async function main() { vscodeExecutablePath, extensionDevelopmentPath, extensionTestsPath: path.resolve(__dirname, 'index'), - extensionTestsEnv: { LEAN4_TEST_FOLDER: 'info', DISABLE_ELAN: '1', DEFAULT_LEAN_TOOLCHAIN: test_version }, + extensionTestsEnv: { LEAN4_TEST_FOLDER: 'info', DEFAULT_LEAN_TOOLCHAIN: test_version }, launchArgs: ['--new-window', '--disable-gpu'], }) diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts index 574b79966..ec46e70f3 100644 --- a/vscode-lean4/test/suite/simple/simple.test.ts +++ b/vscode-lean4/test/suite/simple/simple.test.ts @@ -2,9 +2,9 @@ import * as assert from 'assert' import { suite } from 'mocha' import * as path from 'path' import * as vscode from 'vscode' -import { isElanDisabled } from '../../../src/config' import { UntitledUri } from '../../../src/utils/exturi' import { logger } from '../../../src/utils/logger' +import { displayInformation } from '../../../src/utils/notifs' import { assertStringInInfoview, closeAllEditors, @@ -16,21 +16,13 @@ import { waitForInfoviewHtml, } from '../utils/helpers' -function getElanMode() { - let mode = '' - if (isElanDisabled()) { - mode = ' no elan ' - } - return mode -} - suite('Lean4 Basics Test Suite', () => { test('Untitled Lean File', async () => { - logger.log(`=================== Untitled Lean File ${getElanMode()} ===================`) - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + logger.log('=================== Untitled Lean File ===================') + displayInformation('Running tests: ' + __dirname) - const lean = await initLean4Untitled('#eval Lean.versionString') - const info = lean.exports.infoProvider + const features = await initLean4Untitled('#eval Lean.versionString') + const info = features.infoProvider assert(info, 'No InfoProvider export') await assertStringInInfoview(info, '4.0.0-nightly-') @@ -59,18 +51,18 @@ suite('Lean4 Basics Test Suite', () => { }).timeout(60000) test('Orphaned Lean File', async () => { - logger.log(`=================== Orphaned Lean File ${getElanMode()} ===================`) - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + logger.log('=================== Orphaned Lean File ===================') + displayInformation('Running tests: ' + __dirname) const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'orphan') - const lean = await initLean4(path.join(testsRoot, 'factorial.lean')) + const features = await initLean4(path.join(testsRoot, 'factorial.lean')) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') const expectedVersion = '5040' // the factorial function works. const html = await waitForInfoviewHtml(info, expectedVersion) - const installer = lean.exports.installer + const installer = features.installer assert(installer, 'No LeanInstaller export') const toolChains = await installer.elanListToolChains(new UntitledUri()) let defaultToolChain = toolChains.find(tc => tc.indexOf('default') > 0) @@ -90,8 +82,8 @@ suite('Lean4 Basics Test Suite', () => { }).timeout(60000) test('Goto definition in a package folder', async () => { - logger.log(`=================== Goto definition in a package folder ${getElanMode()} ===================`) - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + logger.log('=================== Goto definition in a package folder ===================') + displayInformation('Running tests: ' + __dirname) // Test we can load file in a project folder from a package folder and also // have goto definition work showing that the LeanClient is correctly @@ -101,9 +93,9 @@ suite('Lean4 Basics Test Suite', () => { // and again using "open folder" mode. const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') - const lean = await initLean4(path.join(testsRoot, 'Main.lean')) + const features = await initLean4(path.join(testsRoot, 'Main.lean')) - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') let expectedVersion = 'Hello:' let html = await waitForInfoviewHtml(info, expectedVersion) diff --git a/vscode-lean4/test/suite/toolchains/toolchain.test.ts b/vscode-lean4/test/suite/toolchains/toolchain.test.ts index a83cc4bec..3a1caad5d 100644 --- a/vscode-lean4/test/suite/toolchains/toolchain.test.ts +++ b/vscode-lean4/test/suite/toolchains/toolchain.test.ts @@ -2,8 +2,8 @@ import * as assert from 'assert' import * as fs from 'fs' import { suite } from 'mocha' import * as path from 'path' -import * as vscode from 'vscode' import { logger } from '../../../src/utils/logger' +import { displayInformation } from '../../../src/utils/notifs' import { assertStringInInfoview, closeAllEditors, @@ -17,16 +17,16 @@ import { suite('Toolchain Test Suite', () => { test('Edit lean-toolchain version', async () => { logger.log('=================== Edit lean-toolchain version ===================') - void vscode.window.showInformationMessage('Running tests: ' + __dirname) + displayInformation('Running tests: ' + __dirname) const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple') - const lean = await initLean4(path.join(testsRoot, 'Main.lean')) + const features = await initLean4(path.join(testsRoot, 'Main.lean')) // turn off the user prompts so restart of lean server happens automatically. - const info = lean.exports.infoProvider + const info = features.infoProvider assert(info, 'No InfoProvider export') - const installer = lean.exports.installer + const installer = features.installer assert(installer, 'No LeanInstaller export') // wait for info view to show up. diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts index aff2950cd..0b8b7386d 100644 --- a/vscode-lean4/test/suite/utils/helpers.ts +++ b/vscode-lean4/test/suite/utils/helpers.ts @@ -4,7 +4,7 @@ import * as os from 'os' import { basename, join } from 'path' import * as vscode from 'vscode' import { DocViewProvider } from '../../../src/docview' -import { Exports } from '../../../src/exports' +import { AlwaysEnabledFeatures, EnabledFeatures, Exports } from '../../../src/exports' import { InfoProvider } from '../../../src/infoview' import { LeanClient } from '../../../src/leanclient' import { LeanClientProvider } from '../../../src/utils/clientProvider' @@ -31,13 +31,12 @@ export function assertAndLog(value: unknown, message: string): asserts value { assert(value, message) } -export async function initLean4(fileName: string): Promise> { +export async function initLean4(fileName: string): Promise { await closeAllEditors() const options: vscode.TextDocumentShowOptions = { preview: false } const lean = await waitForActiveExtension('leanprover.lean4', 60) assertAndLog(lean, 'Lean extension not loaded') - assertAndLog(lean.exports.isLean4Project, 'Lean extension is not a lean4 project') assertAndLog(lean.isActive, 'Lean extension is not active') logger.log(`Found lean package version: ${lean.packageJSON.version}`) @@ -45,11 +44,28 @@ export async function initLean4(fileName: string): Promise { + await closeAllEditors() + const options: vscode.TextDocumentShowOptions = { preview: false } + + const lean = await waitForActiveExtension('leanprover.lean4', 60) + assertAndLog(lean, 'Lean extension not loaded') + assertAndLog(lean.isActive, 'Lean extension is not active') + logger.log(`Found lean package version: ${lean.packageJSON.version}`) + + const doc = await vscode.workspace.openTextDocument(fileName) + await vscode.window.showTextDocument(doc, options) + + await waitForActiveEditor(basename(fileName)) + return lean.exports.alwaysEnabledFeatures } export async function insertText(text: string): Promise { @@ -77,7 +93,7 @@ export async function deleteAllText(): Promise { }) } -export async function initLean4Untitled(contents: string): Promise> { +export async function initLean4Untitled(contents: string): Promise { // make sure test is always run in predictable state, which is no file or folder open await closeAllEditors() @@ -95,13 +111,14 @@ export async function initLean4Untitled(contents: string): Promise { + logger.log('Waiting for Lean 4 feature exports of extension to be loaded...') + const timeoutPromise: Promise = new Promise((resolve, _) => + setTimeout(() => resolve(undefined), timeout), + ) + const allFeatures: EnabledFeatures | undefined = await Promise.race([exports.allFeatures(), timeoutPromise]) + assertAndLog(allFeatures, 'Lean 4 features did not activate.') + logger.log('Lean 4 feature exports loaded.') + return allFeatures +} + +export async function assertLean4FeaturesNotLoaded(exports: Exports) { + logger.log('Waiting for Lean 4 feature exports of extension to be loaded...') + const allFeatures: EnabledFeatures | undefined = await new Promise(async (resolve, _) => { + setTimeout(() => resolve(undefined), 5000) + await exports.allFeatures() + }) + assertAndLog(!allFeatures, 'Lean 4 features activated when they should not have been activated.') + logger.log('Lean 4 features correctly did not load.') +} + export async function waitForActiveEditor(filename = '', retries = 60, delay = 1000): Promise { let count = 0 while (!vscode.window.activeTextEditor && count < retries) { @@ -221,11 +259,15 @@ export async function waitForActiveEditor(filename = '', retries = 60, delay = 1 return editor } -export async function waitForActiveInfoProvider(exports: Exports, retries = 60, delay = 1000): Promise { +export async function waitForActiveInfoProvider( + features: EnabledFeatures, + retries = 60, + delay = 1000, +): Promise { logger.log('Waiting for info view provider to be loaded...') let count = 0 - while (!exports.infoProvider) { + while (!features.infoProvider) { count += 1 if (count >= retries) { logger.log('Info view provider did not load.')