Elan installation fails on Windows

[Timmmm]

Using Windows 10, if I install the Lean VSCode extension and click to install the Lean version manager I get some nonsense code signing error:

For google:

File C:\program files\powershell\7\Modules\PSReadline\PSReadLine.format.ps1xml is published by CN=Microsoft Corporation, O=Microsoft Corporation, L=Redmond, S=Washington, C=US and is not trusted on your system. Only run scripts from trusted publishers.

[Timmmm]

Following the manual instructions I get this error:

> powershell -ExecutionPolicy Bypass -f elan-init.ps1
info: downloading installer to C:\Users\Tim\AppData\Local\Temp\
Download failed for https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip
1

[Timmmm]

The error message can be improved via Write-Host $_ (PR). Then this turns out to give the same error as #349.

Download failed for https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip
Object reference not set to an instance of an object.
1

[mhuisi]

There seem to be three separate issues in this report:

1. PowerShell can sometimes ask for input when running the installation script in VS Code, causing it to fail. I believe that this issue is ultimately a duplicate of installation fails if a startup script in the terminal asks for input #558. The specific instance of this problem in your case seems to be caused by a strange system setup: why is PSReadLine, an auto-loaded script by Microsoft, not trusted on your system? It seems like your PowerShell installation is also very old, since it prompts about PowerShell Core 6.0, which was released in 2016.
2. Downloading Elan from https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip appears to fail when running the installer manually. If the issue still occurs with an up-to-date Windows 10 and PowerShell version (e.g. PowerShell 7 - please confirm this before making a report, it's unlikely that someone will work on this issue if it is caused by your system being outdated since before 2016), you should report this over at leanprover/elan.
3. The error message when the manual installer fails is bad.

[Timmmm]

If the issue still occurs with an up-to-date Windows 10 and PowerShell version (e.g. PowerShell 7 - please confirm this before making a report, it's unlikely that someone will work on this issue if it is caused by your system being outdated since before 2016)

Yeah I'm on an up-to-date Windows 10 with PowerShell 7.

This PR fixes the download failure: leanprover/elan#155

This PR fixes the bad error message: leanprover/elan#153

I guess technically this issue should be in the elan repo since the fixes are there.

[mhuisi]

Thanks :-)

Since you have essentially already reported issue 2 and 3 at the Elan repository and issue 1 is a duplicate of #558, do you agree that this issue in vscode-lean4 can be closed?