Can't get olean cache

Stream: new members

[Winston Yin]

I seem to be having some trouble creating a new project using the current version of mathlib. I used leanproject new xxx, which gave me a new directory xxx with all the source .lean files in _target/deps/mathlib/, but the src/ directory, where .olean files are supposed to be, is entirely empty. When I ran leanproject get-cache or get-mathlib-cache, the src/ directory doesn't get populated. In fact, it downloads fd48ac55697cadbf777009e95b963aa142310a84.tar.xz into ~/.mathlib/. When I unpack it, it actually has all the .olean files of an older version of mathlib (it doesn't have algebra/monoid_algebra/basic.olean).

What's going on, and how can I continue?

[Winston Yin]

(deleted)

[Winston Yin]

I could just run leanproject build under _target/deps/mathlib/ but I'm trying to avoid needlessly torturing my computer

[Eric Rodriguez]

if you want to work on mathlib itself, you shouldn't make a new project, but instead clone mathlib using leanproject get mathlib

[Eric Rodriguez]

if you're working on a new project this is as intended, mathlib is only in the deps (and it should unpack the oleans there after getting them) and then you can just import + use in your project

[Winston Yin]

I just did leanproject get mathlib, which gave me all the .lean and .olean files under src/. Will Lean know to prioritise the use of .olean files when parsing new files under src/? I created a test.lean, but even the import line is taking forever to parse.

[Winston Yin]

And it eventually fails with excessive memory consumption

[Eric Rodriguez]

oh, did you restart the lean server after getting the cache?

[Winston Yin]

No. How do I do that

[Kevin Buzzard]

Exit VS code and restart it

[Winston Yin]

Hmm I've done that multiple times

[Winston Yin]

All I wanted to do is to update my version of mathlib but the process I went through the first time doesn't seem to yield the same results this time

[Winston Yin]

Namely, using leanproject new to get mathlib, etc

[Winston Yin]

I've also upgraded Lean from 3.30 to 3.32. Does that somehow change things?

[Eric Wieser]

I'm confused; are you trying to work on mathlib, or use mathlib in a different project?

[Winston Yin]

I'm trying to work on mathlib

[Winston Yin]

I now have all the lean and olean files all under src/, but the difficulty seems to be excessive memory consumption when I try to import topology.basic, for example

[Eric Rodriguez]

so for me, typing this into the terminal works out of the box:

$ leanproject get mathlib
(git stuff)
(leanproject progressbar)
$ code mathlib

trust the project, and then make a new file with the Lean extension, and import topology.basic. What happens if you try exactly those steps?

[Kevin Buzzard]

If you want to get your mathlib project working, change into the root directory of your local clone and type leanproject get-cache. Then restart VS Code.

[Kevin Buzzard]

Or, if you've not made any local changes yet, nuke your clone and do what Eric suggests

[Winston Yin]

I did exactly what Eric suggested, which gives this output in the terminal:

Cloning from git@github.com:leanprover-community/mathlib.git
configuring mathlib 0.1
Looking for local mathlib oleans
Found local mathlib oleans

[Winston Yin]

Then, I opened VSCode anew, created a new file under src/ called test.lean, typed import topology.basic. The result is my laptop fan taking off and an eventual excessive memory consumption after several mins

[Eric Rodriguez]

the code command should've opened vscode itself; did that not work? also, you used "open folder" right?

[Winston Yin]

I'm on mac, so I don't have code in terminal

[Winston Yin]

But I opened VSCode and opened the mathlib folder

[Winston Yin]

(After quitting it entirely)

[Eric Rodriguez]

m1 mac or normal mac? iirc there's some special instructions fir m1s somewhere

[Winston Yin]

Intel mac

[Winston Yin]

My other folder named mathlib_old created a couple months ago is still working fine

[Eric Rodriguez]

hmm, I don't want you to break your only working mathlib but I'm otherwise out of ideas. two things; does elan as a command work? and also, could you maybe try copying that folder somewhere and running leanproject up on the clone, and see if that works?

[Winston Yin]

Yes, elan works

[Eric Rodriguez]

because you said you upgradede lean but that usually happens transparently for us through elan

[Winston Yin]

Couldn't pull from a relevant git remote. You may try to git pull manually and then run leanproject get-cache

[Eric Rodriguez]

git remote -v?

[Winston Yin]

Nothing comes out of git remote -v

[Winston Yin]

My working mathlib_old was created by leanproject new

[Winston Yin]

And it gives me a src/ directory containing only the .olean files, while _target/deps/mathlib/ contains only the .lean files

[Winston Yin]

This time, however, leanproject new gave me a _target/deps/mathlib/ containing .olean AND .lean files, while the src/ directory is empty

[Eric Rodriguez]

the second is the standard setup, the fact that the first works at all is weird to me

[Winston Yin]

Hmm. All I did was use the recommended commands both times.

[Winston Yin]

Another difference I found was that the old one's leanpkg.path is

builtin_path
path ./src

while the new one's is

builtin_path
path _target/deps/mathlib/src
path ./src

[Winston Yin]

The old one was lean 3.30.0 while new one is lean 3.32.1, if that's relevant at all

[Winston Yin]

And I used elan to upgrade lean from 3.30 to 3.32

[Winston Yin]

I've got to go now, but I'll come back to finish debugging this. Thanks for your help!

[Eric Wieser]

If you're working on mathlib itself there should be no .target/deps/mathlib folder

[Winston Yin]

You're right. My leanproject get mathlib result only has everything within the src/ directory, but the problem is, import whatever takes forever and ends in excessive memory consumption. I saw @Christopher Upshaw's thread above titled "mathlib hanging". Maybe that's relevant?

[Kevin Buzzard]

You should never be using elan directly at all. It doesn't really make sense to say "I used elan to upgrade lean" -- the version of lean used is determined by the nearest leanpkg.toml file, one does not have a specific version of lean installed on one's system, one typically has many versions of lean installed, and the system, not the user chooses which one to use.

Let's start again. Go to a place with no mathlib subdirectory. Type leanproject get mathlib. Now change into the new mathlib subdirectory which just appeared and type lean --make src. Does this command terminate after a few seconds with no output? If so, it's working. If not, your installation is broken in an interesting way (you have managed to corrupt your lean set-up somehow) and it will be quite a bore to debug it via chat.

[Winston Yin]

Thanks for explaining. lean --make src seems to be compiling through everything with no end in sight, so I guess my install is broken :(