Cannot install LEAN4

Stream: new members

[Jordi Majó]

I've tried to install LEAN4 through the VS Code extension and keep getting the following error:

PS G:\My Drive\090 LEAN> Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -Destination "elan-init.ps1"
Start-BitsTransfer : Access is denied. (Exception from HRESULT: 0x80070005 (E_ACCESSDENIED))
At line:1 char:1

• Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanpro ...
• ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  + CategoryInfo : NotSpecified: (:) [Start-BitsTransfer], UnauthorizedAccessException
  + FullyQualifiedErrorId : System.UnauthorizedAccessException,Microsoft.BackgroundIntelligentTransfer.Management.NewBitsTransferCommand

PS G:\My Drive\090 LEAN> Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
PS G:\My Drive\090 LEAN> $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:nightly
.\elan-init.ps1 : The term '.\elan-init.ps1' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name, or if a path was included, verify that the path
is correct and try again.
At line:1 char:7

• $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4: ...
• ~~~~~~~~~~~~~~~
  + CategoryInfo : ObjectNotFound: (.\elan-init.ps1:String) [], CommandNotFoundException
  + FullyQualifiedErrorId : CommandNotFoundException

PS G:\My Drive\090 LEAN> Write-Host "elan-init returned [$rc]"
elan-init returned []
PS G:\My Drive\090 LEAN> del .\elan-init.ps1
del : Cannot find path 'G:\My Drive\090 LEAN\elan-init.ps1' because it does not exist.
At line:1 char:1

• del .\elan-init.ps1
• ~~~~~~~~~~~~~~~~~~~
  + CategoryInfo : ObjectNotFound: (G:\My Drive\090 LEAN\elan-init.ps1:String) [Remove-Item], ItemNotFoundException
  + FullyQualifiedErrorId : PathNotFound,Microsoft.PowerShell.Commands.RemoveItemCommand

PS G:\My Drive\090 LEAN> if ($rc -ne 0) {

Read-Host -Prompt "Press ENTER to continue"

}
Press ENTER to continue:

Does anyone know a fix for this?
Any help will be welcome.

Thanks,

Jordi

[Mauricio Collares]

Do you have write access to G:\My Drive\090 LEAN?

[Mauricio Collares]

If not, try starting VS Code from another folder

[Jordi Majó]

Mauricio Collares said:

If not, try starting VS Code from another folder

Hi Mauricio, I do have access to the drive. I will try another drive anyway...

[Jordi Majó]

Starting VS Code from a local folder I have full access to doesn't work either...

Lean (version 4.0.0-nightly-2023-08-30, commit b8084d54e32c, Release)
elan 2.0.1 (04475bbb5 2023-07-24)
Watchdog error: no such file or directory (error code: 2)
[Error - 12:58:26 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

Any other ideas?

Thanks,

Jordi

[Mauricio Collares]

You can try downloading https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 and manually running the two commands VS Code ran, namely

Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
$rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:nightly

under PowerShell (in the folder containing the file you downloaded, of course), to see if it gets around whatever permission problem is causing the install to fail.

[Mauricio Collares]

Or, said it another way, try following the Windows steps at https://github.com/leanprover/elan#manual-installation to install Elan

[Mauricio Collares]

You can also download https://github.com/leanprover/elan/releases/download/v2.0.1/elan-x86_64-pc-windows-msvc.zip directly and run the executable installer

[Jordi Majó]

Hi Mauricio et al. ,
I tried the stand alone installer as you suggested in your last sentence. It worked fine, but now, when I try to start the server from within VS Code, I guet the following:

info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2023-09-01
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 4.0.0-nightly-2023-09-01, commit 77600c56b6ec, Release)
elan 2.0.1 (04475bbb5 2023-07-24)
Watchdog error: no such file or directory (error code: 2)
[Error - 10:46:16 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

Any Ideas?
Any help will be welcome.

Thanks,

Jordi

[Mauricio Collares]

What project are you opening? Is it one you created yourself? If so, are you using the VS Code "open workspace" option to open the folder containing the "lean-toolchain" file?

[Mauricio Collares]

You can try cloning https://github.com/leanprover-community/mathematics_in_lean if you want to try with a known-good project

[Mauricio Collares]

Lean does not work very well with standalone files