fix: Elan installation in PowerShell ConstrainedLanguage mode

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."

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."

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`

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-<file name>`. 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.

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