From 47146e760029b5662652bae6a89a3ee33417bd33 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Wed, 11 Nov 2026 19:26:37 +0000 Subject: [PATCH] fix: install Elan in PowerShell ConstrainedLanguage mode --- .../media/guide-installLean-windows.md | 8 +- .../scripts/elan-install/install-windows.ps1 | 7 +- vscode-lean4/scripts/installation-scripts.md | 3 + vscode-lean4/test/README.md | 2 +- .../unit/elanInstallLanguageModes.test.ts | 160 ++++++++++++++++++ 5 files changed, 177 insertions(+), 3 deletions(-) create mode 100644 vscode-lean4/test/unit/elanInstallLanguageModes.test.ts diff --git a/vscode-lean4/media/guide-installLean-windows.md b/vscode-lean4/media/guide-installLean-windows.md index bbf718de..b51c16f1 100644 --- a/vscode-lean4/media/guide-installLean-windows.md +++ b/vscode-lean4/media/guide-installLean-windows.md @@ -55,7 +55,13 @@ Then the following script installs Elan: # Download the Elan installation script at https://github.com/leanprover/elan/blob/master/elan-init.ps1 and run it. Elan will be installed to `%USERPROFILE%\.elan`. try { $installCode = (Invoke-WebRequest -Uri "https://elan.lean-lang.org/elan-init.ps1" -UseBasicParsing -ErrorAction Stop).Content - $installer = [ScriptBlock]::Create([System.Text.Encoding]::UTF8.GetString($installCode)) + # PowerShell in ConstrainedLanguage mode does not allow the method calls in the first branch. In that mode, `[uri]::UnescapeDataString` decodes the installation script, and `Invoke-Expression` makes the script block. + if ($ExecutionContext.SessionState.LanguageMode -eq 'FullLanguage') { + $installer = [ScriptBlock]::Create([System.Text.Encoding]::UTF8.GetString($installCode)) + } else { + $installText = [uri]::UnescapeDataString(-join ($installCode | ForEach-Object { '%{0:X2}' -f $_ })) + $installer = Invoke-Expression "{`n$installText`n}" + } $rc = & $installer -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable | Select-Object -Last 1 } catch { Write-Host "Downloading and running the Elan installer failed." diff --git a/vscode-lean4/scripts/elan-install/install-windows.ps1 b/vscode-lean4/scripts/elan-install/install-windows.ps1 index 9141fda0..f580315d 100644 --- a/vscode-lean4/scripts/elan-install/install-windows.ps1 +++ b/vscode-lean4/scripts/elan-install/install-windows.ps1 @@ -8,7 +8,12 @@ $ProgressPreference = 'SilentlyContinue' try { $installCode = (Invoke-WebRequest -Uri "https://elan.lean-lang.org/elan-init.ps1" -UseBasicParsing -ErrorAction Stop).Content - $installer = [ScriptBlock]::Create([System.Text.Encoding]::UTF8.GetString($installCode)) + if ($ExecutionContext.SessionState.LanguageMode -eq 'FullLanguage') { + $installer = [ScriptBlock]::Create([System.Text.Encoding]::UTF8.GetString($installCode)) + } else { + $installText = [uri]::UnescapeDataString(-join ($installCode | ForEach-Object { '%{0:X2}' -f $_ })) + $installer = Invoke-Expression "{`n$installText`n}" + } $rc = & $installer -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable | Select-Object -Last 1 } catch { Write-Host "Downloading and running the Elan installer failed." diff --git a/vscode-lean4/scripts/installation-scripts.md b/vscode-lean4/scripts/installation-scripts.md index 719dcce6..3c116632 100644 --- a/vscode-lean4/scripts/installation-scripts.md +++ b/vscode-lean4/scripts/installation-scripts.md @@ -24,6 +24,9 @@ On computers with AppLocker or WDAC, PowerShell can run in ConstrainedLanguage m - `Expand-Archive` in `elan-init.ps1` loads a script module. Thus the extension and the CI action start Windows PowerShell with the execution policy `Bypass`. In a terminal, the manual script must set this policy itself. It puts this script into a second script block (`windowsManualScript` in `src/utils/leanInstaller.ts`). This block sets `Bypass` for the process. At the end, also after a `throw`, it sets the old policy of the process again (`finally`). - The script block does not keep the proxy credentials in its scope. `DefaultWebProxy` is an object of the process, so its credentials stay set after the script. Later downloads in the session then also give the Windows credentials to the proxy. - With a progress display, `Invoke-WebRequest` of Windows PowerShell 5.1 downloads much more slowly. Thus the script sets `$ProgressPreference` to `SilentlyContinue`. `elan-init.ps1` also downloads Elan with `Invoke-WebRequest`. It runs in a child scope of the script block, so it uses this value too. +- ConstrainedLanguage mode permits method calls only on a small set of types. Thus `[ScriptBlock]::Create` and `GetString` fail in this mode. There, the script puts the text of `elan-init.ps1` between `{` and `}`, and `Invoke-Expression` returns this text as a script block. The line that runs the installer is the same in the two modes. The script block is not a file, so the execution policy does not apply to it. +- In ConstrainedLanguage mode, the script also decodes the bytes of `elan-init.ps1` as UTF-8. `[uri]` is one of the types on which this mode permits method calls. Thus the script writes each byte as `%XX`, and `[uri]::UnescapeDataString` decodes this text as UTF-8. +- `test/unit/elanInstallLanguageModes.test.ts` runs the script in the two modes, with a stub for `elan-init.ps1`. The stub contains characters that are not ASCII. The test uses PowerShell 7 and, on Windows, also Windows PowerShell. - `elan-init.ps1` returns 0 or 1. The script uses only the last output of `elan-init.ps1` (`Select-Object -Last 1`). We do not pin `elan-init.ps1`, and a later version can write more objects to the pipeline. Then `$rc` is an array, and `$rc -ne 0` is true when the array contains a value other than 0. ## `elan-install/install-unix.sh` diff --git a/vscode-lean4/test/README.md b/vscode-lean4/test/README.md index ef35081f..1bffa81b 100644 --- a/vscode-lean4/test/README.md +++ b/vscode-lean4/test/README.md @@ -5,7 +5,7 @@ - `vscode-test-cli/`: integration tests that run in the VS Code extension host through `@vscode/test-cli`. Each file runs in its own VS Code instance, with the label `cli-`. Elan must be installed. VS Code opens the fixture `lean-project` as the workspace, except for `adhoc` (no folder) and `multi-root` (the multi-root workspace in `fixtures/multi-root/`). To change this, edit `workspaceOf` in `.vscode-test.mjs`. - `wdio/`: UI tests of the InfoView through `wdio-vscode-service`. Only these tests can read the content of a webview. - `network/`: tests that download elan, a Lean toolchain and Mathlib. CI runs them only on the nightly schedule and on manual dispatch. On a GitHub-hosted Windows runner, `git-install.test.ts` also uninstalls Git and installs it again (see "Test home"). -- `unit/`: pure TypeScript tests for vitest. They do not use VS Code. +- `unit/`: pure TypeScript tests for vitest. They do not use VS Code. `elanInstallLanguageModes.test.ts` runs a script with PowerShell 7 (`pwsh`) and, on Windows, also with Windows PowerShell. If a program is not available, vitest skips its tests. - `grammar/`: snapshot tests for the TextMate grammars. See `grammar/README.md`. - `helpers/`: shared code for the tests. See the helper map at the end of this file. - `fixtures/`: Lean projects and files that the tests open. diff --git a/vscode-lean4/test/unit/elanInstallLanguageModes.test.ts b/vscode-lean4/test/unit/elanInstallLanguageModes.test.ts new file mode 100644 index 00000000..916a017c --- /dev/null +++ b/vscode-lean4/test/unit/elanInstallLanguageModes.test.ts @@ -0,0 +1,160 @@ +import { execFile, spawnSync } from 'node:child_process' +import * as fs from 'node:fs' +import * as http from 'node:http' +import type { AddressInfo } from 'node:net' +import * as path from 'node:path' +import { afterAll, beforeAll, describe, expect, it } from 'vitest' +import { withoutPSModulePath } from '../../src/utils/envPath' + +// On computers with AppLocker or WDAC, PowerShell can run in +// ConstrainedLanguage mode. This mode permits method calls only on a small set +// of types. `scripts/elan-install/install-windows.ps1` must also install Elan +// in this mode (`scripts/installation-scripts.md`). +// +// This test runs the script in the two language modes. A local server gives a +// stub for `elan-init.ps1`, so the test installs nothing and can run on all +// platforms. The stub has the same structure as `elan-init.ps1`: a help +// comment, a `param` block, and a `return` with the exit code. +// +// The test runs the script with PowerShell 7 (`pwsh`) on all platforms. On +// Windows, it also runs the script with Windows PowerShell, which the +// extension uses. A session of these programs can set its own language mode to +// ConstrainedLanguage. If a program is not available, vitest skips its tests. +// The GitHub-hosted runners have `pwsh`. + +type Shell = { name: string; exe: string; env: NodeJS.ProcessEnv; available: boolean } + +const shellArgs = ['-NoProfile', '-NonInteractive'] + +// `withoutPSModulePath` explains why Windows PowerShell must not get +// `PSModulePath`. The path is the path of `getPowerShellPath` in +// `src/config.ts`. +const shells: Shell[] = [ + { + name: 'PowerShell 7', + exe: 'pwsh', + env: process.env, + available: spawnSync('pwsh', [...shellArgs, '-Command', 'exit 0']).status === 0, + }, + { + name: 'Windows PowerShell', + exe: path.win32.join( + process.env.windir || process.env.SystemRoot || 'C:\\Windows', + 'System32', + 'WindowsPowerShell', + 'v1.0', + 'powershell.exe', + ), + env: withoutPSModulePath(process.env), + available: process.platform === 'win32', + }, +] + +const elanInitUrl = 'https://elan.lean-lang.org/elan-init.ps1' + +// Characters that UTF-8 encodes with 2, 3 and 4 bytes. The stub contains them, +// and the script must decode them correctly in the two language modes. +const nonAsciiText = '\u{e9}\u{2713}\u{1f600}' +// The UTF-16 codes of `nonAsciiText`. The stub writes the codes and not the +// characters, so that the output encoding of the shell has no effect on the +// test. +const nonAsciiCodes = Array.from({ length: nonAsciiText.length }, (_, i) => nonAsciiText.charCodeAt(i)).join(',') + +// The stub writes its language mode and its arguments to the host. It also +// writes a second object to the pipeline before the exit code: the script must +// use only the last object. +function elanInitStub(exitCode: number): string { + return [ + '<#', + '.SYNOPSIS', + ' A stub for `elan-init.ps1`.', + '#>', + 'param(', + ' [bool] $NoPrompt = 0,', + ' [string] $DefaultToolchain = ""', + ')', + 'Write-Host "stub: mode=$($ExecutionContext.SessionState.LanguageMode) NoPrompt=$NoPrompt DefaultToolchain=$DefaultToolchain"', + `Write-Host "stub: codes=$([int[]][char[]]'${nonAsciiText}' -join ',')"`, + '"an output that is not the exit code"', + `return ${exitCode}`, + '', + ].join('\n') +} + +describe('scripts/elan-install/install-windows.ps1', () => { + const extensionDir = path.join(__dirname, '..', '..') + const installScript = fs.readFileSync( + path.join(extensionDir, 'scripts', 'elan-install', 'install-windows.ps1'), + 'utf8', + ) + const toolchain = /-DefaultToolchain (\S+)/.exec(installScript)?.[1] + + // `/0/elan-init.ps1` gives a stub that returns 0, `/1/elan-init.ps1` gives + // a stub that returns 1. The content type is the content type of + // `elanInitUrl`. With this type, `Invoke-WebRequest` gives the content as + // bytes. + let server: http.Server + beforeAll(async () => { + server = http.createServer((req, res) => { + res.writeHead(200, { 'Content-Type': 'application/octet-stream' }) + res.end(elanInitStub(req.url?.startsWith('/0/') ? 0 : 1)) + }) + await new Promise(resolve => server.listen(0, '127.0.0.1', resolve)) + }) + afterAll(async () => { + await new Promise(resolve => server.close(resolve)) + }) + + // Runs the install script with `shell` in the language mode `mode`, with + // the stub that returns `stubExitCode`. `-EncodedCommand` prevents quoting + // problems. With it, PowerShell writes errors as XML, unless the output + // format is `Text`. `spawnSync` cannot be used here, because it blocks the + // server. + function runInstallScript( + shell: Shell, + mode: string, + stubExitCode: number, + ): Promise<{ exitCode: number; output: string }> { + expect(installScript).toContain(elanInitUrl) + const { port } = server.address() as AddressInfo + const script = installScript.replace(elanInitUrl, `http://127.0.0.1:${port}/${stubExitCode}/elan-init.ps1`) + const command = `$ExecutionContext.SessionState.LanguageMode = '${mode}'\n${script}` + const encodedCommand = Buffer.from(command, 'utf16le').toString('base64') + return new Promise(resolve => { + const args = [...shellArgs, '-OutputFormat', 'Text', '-EncodedCommand', encodedCommand] + execFile(shell.exe, args, { env: shell.env }, (error, stdout, stderr) => { + const exitCode = error === null ? 0 : typeof error.code === 'number' ? error.code : -1 + resolve({ exitCode, output: stdout + stderr }) + }) + }) + } + + const modes = ['FullLanguage', 'ConstrainedLanguage'] + const timeoutMs = 60_000 + + for (const shell of shells) { + describe.skipIf(!shell.available)(`with ${shell.name}`, () => { + it.each(modes)( + 'runs the Elan installer in %s mode', + async mode => { + const { exitCode, output } = await runInstallScript(shell, mode, 0) + expect(output).toContain(`stub: mode=${mode} NoPrompt=True DefaultToolchain=${toolchain}`) + // The lines of the output end with `\r\n` on Windows. + expect(output.split(/\r?\n/)).toContain(`stub: codes=${nonAsciiCodes}`) + expect(exitCode, output).toBe(0) + }, + timeoutMs, + ) + + it.each(modes)( + 'fails in %s mode when the Elan installer fails', + async mode => { + const { exitCode, output } = await runInstallScript(shell, mode, 1) + expect(output).toContain(`stub: mode=${mode} NoPrompt=True DefaultToolchain=${toolchain}`) + expect(exitCode, output).toBe(1) + }, + timeoutMs, + ) + }) + } +})