Lean vscode high ram usage

Stream: new members

[bradley]

I have installed Lean 3.51.1 along with the Lean3 vscode extension which I need for a university module. I cannot seem to get mathlib working. I have attempted multiple fresh installs and ran leanproject new, however during the installation it ends with an error:

% leanproject new leanFolder
> cd leanFolder
> git init -q
> git checkout -b lean-3.51.1
Switched to a new branch 'lean-3.51.1'
configuring leanFolder 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 387724, done.
remote: Counting objects: 100% (3642/3642), done.
remote: Compressing objects: 100% (1038/1038), done.
remote: Total 387724 (delta 3289), reused 2687 (delta 2602), pack-reused 384082
Receiving objects: 100% (387724/387724), 218.51 MiB | 9.95 MiB/s, done.
Resolving deltas: 100% (310642/310642), done.
> git checkout --detach 4e976107aa81b41822bd5bb2b15c90b1c8a2aa15    # in directory _target/deps/mathlib
HEAD is now at 4e976107aa feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)
configuring leanFolder 0.1
mathlib: trying to update _target/deps/mathlib to revision 4e976107aa81b41822bd5bb2b15c90b1c8a2aa15
> git checkout --detach 4e976107aa81b41822bd5bb2b15c90b1c8a2aa15    # in directory _target/deps/mathlib
HEAD is now at 4e976107aa feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)
Looking for mathlib oleans for 4e976107aa
  locally...
  remotely...
HTTPSConnectionPool(host='oleanstorage.azureedge.net', port=443): Max retries exceeded with url: /mathlib/4e976107aa81b41822bd5bb2b15c90b1c8a2aa15.tar.xz (Caused by NameResolutionError("<urllib3.connection.HTTPSConnection object at 0x103065450>: Failed to resolve 'oleanstorage.azureedge.net' ([Errno 8] nodename nor servname provided, or not known)"))

From here if i attempt to use 'import tactic' anywhere within a lean file, my system becomes more unresponsive and RAM usage becomes very high. I'm assuming it has something to do with not being able to get the mathlib olean files? Any help would be appreciated, I am on MacOS Sonoma and used homebrew to install lean3

[Mauricio Collares]

Yes, it has to do with the error fetching oleans. There has been some cloud issues with the cache servers recently, and I am not 100% sure the olean cache server for mathlib3 will come back given that everyone has migrated to Lean 4 (it probably will, though).

[Mauricio Collares]

Is there any chance you can convince your professor to migrate to Lean 4 in a future version of the course?

[bradley]

It has been acknowledged, but as with most courses things take a long time to get moving unfortunately :(
Is there any other way to retrieve the oleans for now? Or just wait and hope it comes up eventually?

[Mauricio Collares]

The nice thing about Lean 3 oleans is that they're distributed in a single zip file, so the mathlib @maintainers can probably just upload the cache corresponding to mathlib3 master somewhere.

[Mario Carneiro]

It should be back already

[Mario Carneiro]

note that mathlib3 cache is tested daily as part of mathport CI

[bradley]

The server? If so I just tried again and was met with the same error:

Looking for mathlib oleans for 4e976107aa
  locally...
  remotely...
HTTPSConnectionPool(host='oleanstorage.azureedge.net', port=443): Max retries exceeded with url: /mathlib/4e976107aa81b41822bd5bb2b15c90b1c8a2aa15.tar.xz (Caused by NameResolutionError("<urllib3.connection.HTTPSConnection object at 0x104abd350>: Failed to resolve 'oleanstorage.azureedge.net' ([Errno 8] nodename nor servname provided, or not known)"))

[bradley]

I believe that is the error I've always had, even from first attempt at running, I'll try again a bit later.
I'm also trying on Linux but i cant seem to install a lean version through elan, I assume because its deprecated

[Mauricio Collares]

Mario Carneiro said:

note that mathlib3 cache is tested daily as part of mathport CI

Wasn't this disabled in mathport#245?

[Mario Carneiro]

that's a good point, it is a bit concerning because we do rely on the cache for usage of the tool by end users

[Monica Omar]

I'm having this problem at the moment too. I've edited some files in one of my mathlib3 projects and am unable to get the cache and docs for it. No clue what to do.

Obviously am porting to Lean4, but I need to also have this running too.

[Mauricio Collares]

Try running leanproject -u "https://oleanstorage.blob.core.windows.net/mathlib/" get-mathlib-cache manually

[Mauricio Collares]

(leanproject currently points to https://oleanstorage.azureedge.net/mathlib/ which doesn't work)

[Sebastian Ullrich]

It should be back on now

[Mauricio Collares]

Now oleanstorage.azureedge.net resolves but leanproject doesn't find any caches with the default URL (https://oleanstorage.blob.core.windows.net/mathlib/ instead of https://oleanstorage.azureedge.net/mathlib/ still works)

[Mauricio Collares]

Working now, thanks! It sometimes takes a few tries, though, I guess some change is propagating.