Xinzhe Xia

Stream: new members

[Xinzhe Xia]

Hi, I'm quite interested in Lean but before getting familiar with the language I found downloading with some errors here:
(copied from troubleshooting in VSCode)
c:\...\Desktop> lean +leanprover/lean4:stable --version

=> Operation failed. Exit code: -4058.

c:\...\Desktop> lean --version

=> Operation failed. Exit code: -4058.

c:\...\Desktop> lean --version

=> Operation failed. Exit code: -4058.
I believe the issue is that the website can't be accessed from my computer or somehow (to be honest I've got no idea what's happening). Could you please help me with the problem? Thanks for reading!

[Utensil Song]

Try using https://github.com/alissa-tung/glean

[Xinzhe Xia]

OK, I'll take a look at the repos

[Xinzhe Xia]

Utensil Song said:

Try using https://github.com/alissa-tung/glean

It's working and it'll be downloaded in 3h.

[Utensil Song]

3h is unexpected, there might be something else wrong with your network other than regional network issue.

[Utensil Song]

Maybe you can DM @Alissa Tung (the author of glean) to discuss further.

[Xinzhe Xia]

I used the SJTUG Mirror, is this affecting the speed?

[Utensil Song]

It should have a positive impact on the speed.

[Alissa Tung]

[Quoting…]

Hello. I hope this tool can work for you. In China, the tool is expected to download things at 10+ MiB/s.

The setup steps are:

1. Close all the VS Code instances, in the complete process it should not be opened
2. Clone the repository of Lean code that you want, and run command cd to set it as current working directory
3. Download glean from SJTU web site, from the generated index
4. Use the glean command to install elan, according to the glean repo README
5. Use the glean command to install Lean, which should be the version in toolchain file of current directory
6. Use the glean command to install packages in the manifest

That’s all, currently glean does not support mathlib4 cache, but downloading source are mirrored using glean

Feel free to concat me if any question

[Alissa Tung]

Also, after the 6th step, try lake build command in command line, instead of opening vscode

[Kevin Buzzard]

If there are regional problems with downloading lean then probably the FRO are interested to hear this. I was at a talk this week where someone from Peking University was claiming that there would be 100 people working with Lean there this summer.

[Alissa Tung]

Kevin Buzzard said:

If there are regional problems with downloading lean then probably the FRO are interested to hear this. I was at a talk this week where someone from Peking University was claiming that there would be 100 people working with Lean there this summer.

The issue is that the GitHub access and its CDN, and the Azure blob storage can not be accessed from China. Thank you for suggestion on FRO. I will try to figure out that I want to write to FRO what should I do.

I am also one of them from Peking U at the workshop. Yes, we are working for this summer. The glean tool is an initial try on solve the issues we meet, and hope I and the team can make more progress.