search

leanprover / elan

The Lean version manager
Apache License 2.0
316 stars 35 forks source link

elan-init.ps1 problems #71

Closed wintersteiger closed 2 years ago

wintersteiger commented 2 years ago

This from the README:

curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -f elan-init.ps1
del elan-init.ps1

did not work for me, because $cmdline is empty and powershell complains about -ArgumentList missing it's parameter (here). Here's the error:

Start-Process : Cannot validate argument on parameter 'ArgumentList'. The argument is null or empty. Provide an argument that is not null or empty, and then try the command again.
At C:\Users\cwinter\elan-init.ps1:89 char:72
+ ... rocess -FilePath "$_dir/elan-init.exe" -ArgumentList $cmdline  -Wait  ...
+                                                          ~~~~~~~~
    + CategoryInfo          : InvalidData: (:) [Start-Process], ParameterBindingValidationException
    + FullyQualifiedErrorId : ParameterArgumentValidationError,Microsoft.PowerShell.Commands.StartProcessCommand

I suspect someone broke the default for $DefaultToolchain? The comments say

.PARAMETER DefaultToolchain
    Which tool chain to setup as your default toolchain, default is 'none'

but a few lines below it's set to empty instead of 'none':

  [string]$DefaultToolchain = "",

(That's on Windows 11, non-admin command prompt.)

Kha commented 2 years ago

/cc @lovettchris

lovettchris commented 2 years ago

See https://github.com/leanprover/elan/pull/72