[davide-pozzoni-uk-gt]

The current Windows installation script breaks under Constrained Language Mode (CLM). It builds the Elan script into a script block in memory before running it with:

$installer = [ScriptBlock]::Create([System.Text.Encoding]::UTF8.GetString($installCode))

Both [System.Text.Encoding]::UTF8.GetString(...) and [ScriptBlock]::Create(...) are method calls, which CLM blocks. The script fails with MethodInvocationNotSupportedInConstrainedLanguage.

This is a follow-up to leanprover/elan#204, which made elan-init.ps1 itself CLM-safe. This PR completes the chain by making vscode-lean4's invocation of the script CLM-safe.

The change wraps the existing logic in a FullLanguage check. In FullLanguage the behaviour is unchanged. Otherwise (CLM) it:

• resolves a temp directory from environment variables (TMP/TEMP/USERPROFILE/SystemRoot); (Equivalent lookup to https://learn.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-gettemppathw)
• downloads elan-init.ps1 to disk via Invoke-WebRequest -OutFile in the temp location;
• removes the mark-of-the-web with Unblock-File;
• runs the file in a child PowerShell process with -ExecutionPolicy Unrestricted; and
• deletes the file afterwards in a finally block (only if it exists).

A file is required for CLM-safe behaviour, because there is no clean CLM-safe way to UTF-8-decode the downloaded byte[] into a string and run it in memory. Writing the bytes straight to disk avoids decoding entirely.

[mhuisi]

Thanks!

We decided to go with #822 instead since a number of things were changed about the Windows installation.