elan update

Stream: lean4

[Mark Encarnación]

I tried running 'elan self update' (on Windows) but ran into this error:

$ elan self update
info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover/elan/releases/download/v1.0.7/elan-.zip' to 'C:\Users\markenc\AppData\Local\Temp\elan-update.7ssnvBWNqktc\elan-.zip'
info: caused by: http request returned an unsuccessful status code: 404

Any suggestions on how I should update elan?

Thanks!

[Leonardo de Moura]

@Mark Encarnación You don't need to use elan self update to get Lean 4 working on Windows. The Quickstart https://github.com/leanprover/lean4/blob/master/doc/quickstart.md is a bit confusing for Windows. After we have installed elan using elan-init.exe. We should do the following for setting the Lean 4 nightly build as the default toolchain.

• Open a terminal
• Add a new toolchain for Lean 4 using the commang

   elan toolchain install leanprover/lean4:nightly

• Make it the default one

   elan default leanprover/lean4:nightly

• We can confirm that Lean 4 is the default toolchain using

lean --version

The rest of the quickstart instructions should work.

[Mac]

@Mark Encarnación what version of elan are you using? The self update command broke on Windows in v1.0.3 and was fixed in v1.0.6.

[Mac]

If you are using a broken elan, you will need to manually update by running the elan-init.exe in the elan-x86_64-pc-windows-msvc.zip downloadable from and in the releases page.

[Mark Encarnación]

Thanks, @Mac. I'm using elan v1.0.6:
$ elan --version
elan 1.0.6 (bf510c5db 2021-05-25)

Thanks, @Leonardo de Moura. Yes, I have Lean4 working, but I also wanted to make sure I have the latest elan, hence I tried running the self update. I will issue the commands you provided so that I will have the nightly build.

[Mac]

@Mark Encarnación Ah. Well, it appears that @Sebastian Ullrich attempt to fix the URL on not-Linux did not actually succeed in fixing the issue. He's on vacation now, so you'll probably have to wait until he gets back to have that issue looked at. In the meantime, you can manually update elan if you want the latest version.

[Mark Encarnación]

Ok, thanks, @Mac. I'm in no hurry.