Unknown error (0x80092012) - The revocation function was una

Stream: lean4

[Jordi Majó]

Hello,

I've tried to install LEAN4 through the VSCode Extension. It run some commands, but I cannot run the lean server.
Whenever I open a lean file in VSCode, I get several errors:

  info: downloading component 'lean'
  Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
  error: could not download nonexistent lean version `leanprover/lean4:master`
  info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/master' to 'C:\Users\Jordi             Majó\.elan\tmp\9s7nmonrfh6ffdwh_file'
  info: caused by: http request returned an unsuccessful status code: 404
  info: downloading component 'lean'
  Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
  error: could not download nonexistent lean version `leanprover/lean4:master`
  info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/master' to 'C:\Users\Jordi Majó\.elan\tmp\rz5j_27gp9xy_ly3_file'
  info: caused by: http request returned an unsuccessful status code: 404
  info: downloading component 'lean'
  error: could not download nonexistent lean version `leanprover/lean4:master`
  info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/master' to 'C:\Users\Jordi       Majó\.elan\tmp\818innyp__3hn6xe_file'
  info: caused by: http request returned an unsuccessful status code: 404
  [Error - 6:51:47 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.
  [Error - 6:51:47 PM] Server initialization failed.
    Message: Pending response rejected since connection got disposed
    Code: -32097 
  [Error - 6:51:47 PM] Lean 4 client: couldn't create connection to server.
    Message: Pending response rejected since connection got disposed
    Code: -32097

Lean Server has stopped unexpectedly.

If I try to install LEAN4 manually with
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

I also get an error
curl: (35) schannel: next InitializeSecurityContext failed: Unknown error (0x80092012) - The revocation function was unable to check revocation for the certificate.

Could someone please help?

Thx,

Jordi

2023_08_29 Update

I've tried to uninstall everything (elan self uninstall) abd reinstall from the VSCode extension.
This time I get the following errors:

PS H:\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 H:\My Drive\090 LEAN> Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
PS H:\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 H:\My Drive\090 LEAN> Write-Host "elan-init returned [$rc]"
elan-init returned []
PS H:\My Drive\090 LEAN> del .\elan-init.ps1
del : Cannot find path 'H:\My Drive\090 LEAN\elan-init.ps1' because it does not exist.
At line:1 char:1

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

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

Read-Host -Prompt "Press ENTER to continue"

}
Press ENTER to continue:

Any help would be most welcome!!

Thanks,

Jordi