problem updating from v4.2.0-rc1 to v4.2.0-rc4

Stream: lean4

[Chris Birkbeck]

I'm trying to update my repo to rc4 from rc1. I tried running curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain followed by lake update but once I've run the curl... and try to run anything else I get the following error:

error: .\lakefile.lean:1:0: error: unknown package 'Init' error: .\lakefile.lean:2:5: error: unknown namespace 'Lake' error: .\lakefile.lean:4:0: error: unexpected identifier; expected command error: .\lakefile.lean:11:17: error: unexpected identifier; expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem' error: .\lakefile.lean: package configuration has errors

I tried deleting the lakefile.olean beforehand and also the lake-packages, but it doesn't seem to help. I'm having this issue with several repos, for example, this one

[Julian Berman]

Can you show what the current contents of your lean-toolchain file are, just in case?

[Chris Birkbeck]

It just has leanprover/lean4:v4.2.0-rc4

[Chris Birkbeck]

This also happens if I simply try and clone a repo running on rc4.

[Julian Berman]

Does it happen if you try to create a new project with lake init using the rc4?

[Julian Berman]

If so that would sound like the install is borked.

[Chris Birkbeck]

Ah yes it also happens when making a new project.

[Chris Birkbeck]

Is there a way to fix the install?

[Sebastian Ullrich]

Very rarely elan just misdownloads a Lean installation and we have no idea why. Try elan toolchain uninstall.

[Chris Birkbeck]

Ok that worked (well the elan toolchain uninstall didn't but deleting the toolchain folder did). Thank you very much for your help!

[Sebastian Ullrich]

Ah yes, sorry, if the toolchain is too malformed elan even refuses to remove it

[Kevin Buzzard]

Remark: to remove a toolchain manually, don't forget to remove the corresponding file in .elan/update-hashes as well.

[Chris Birkbeck]

Kevin Buzzard said:

Remark: to remove a toolchain manually, don't forget to remove the corresponding file in .elan/update-hashes as well.

Oh I didn't do this, but its working now, so maybe I got lucky ? I'm not sure how to check if something is broken

[Kevin Buzzard]

Maybe if you re-installed it again immediately and it worked, then you're OK. Sometimes (perhaps in the past?) if you removed the directory but not the update-hashes file then you ended up in a state where you could neither install nor remove the toolchain.

[Julian Berman]

@Sebastian Ullrich does/could/should elan verify what it downloads against some checksum file when it downloads the (presumably) tarball, so it's at least possible to report out "something is probably up with the download"?

[Julian Berman]

(one that would presumably have to be optionally published alongside any release artifacts)

[Scott Morrison]

Kevin Buzzard said:

Remark: to remove a toolchain manually, don't forget to remove the corresponding file in .elan/update-hashes as well.

If you have a recent elan I think this is no longer necessary.

[Scott Morrison]

(And in fact you can delete your entire .elan/update-hashes directory and it will not come back!)

[Sebastian Ullrich]

That version of elan has not been released quite yet!