Excessive memory consumption

Stream: new members

[Haruhisa Enomoto]

I'm working on a git branch of mathlib. After I eddited an existing file (algebra/group/units.lean), I opened my own lean file, and lean didn't respond and said the following error at import part:
"invalid import: data.option.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)"
How should I do?
What I did is: restart VS code and Lean, commit changes and execute leanproject mk-cache and leanproject get-cache in git bash.

[Eric Wieser]

leanproject mk-cache just saves the files you currently have compiled

[Eric Wieser]

When you run get-cache does it say "fetching remote oleans" or "using local oleans"

[Haruhisa Enomoto]

It says:

$ leanproject get-cache
Looking for mathlib oleans for 25a62a84e1
  locally...
  Found local mathlib oleans
Using matching cache
Applying cache
  files extracted: 2421 [01:03, 37.92/s]

so probably it used local oleans.

[Haruhisa Enomoto]

Should I use leanproject build?

[Eric Wieser]

You've poisoned your cache with useless oleans

[Eric Wieser]

leanproject build would create new ones, but will take a long time

[Eric Wieser]

Have you pushed your changes to github at all? If so, then it can build you a better cache (without using your CPU time and electricity!)

[Eric Wieser]

@Patrick Massot, should mk-cache give a warning / overridable error if the oleans are out of date? Is "out of date oleans" something we can actually detect right now?

[Haruhisa Enomoto]

Thanks, so I shouldn't have usedleanproject mk-cache.
Now I pushed it to github, so what should I do next?

[Haruhisa Enomoto]

I used leanproject --force-download get-cache, and problem went away! Thanks!

[Eric Wieser]

I forgot that option existed; indeed, that's exactly the right solution

[Eric Wieser]

mk-cache is mainly useful for if you started a local build, but then decide to switch branch to work on something else. When you reload the cache, you'll be able to resume your build where you left off

[Eric Wieser]

Local builds are often useful if you edit really_basic_file.lean and run lean --make mostly_basic_file.lean; rather than pushing to github and waiting an hour or two for it to build everything

[Jireh Loreaux]

Just for future reference, you could always just delete the poisoned cache directly. On Linux they are stored in ~/.mathlib. I'm not sure where they are on another OS.

[Patrick Massot]

Eric Wieser said:

Patrick Massot, should mk-cache give a warning / overridable error if the oleans are out of date? Is "out of date oleans" something we can actually detect right now?

I never use this command myself. I'm open to any modification.

[Haruhisa Enomoto]

What's the usual way when modifying many imported files?
I modified such a file again, and I run lean --make for it, but lean was very slow and I had to commit and push it to github and wait.
Is this a usual case?

[Ruben Van de Velde]

If you change files that many other files depend on, yeah, that's common

[Haruhisa Enomoto]

OK, I didn't know that, thanks!

[Andrew Helwer]

I just installed lean and mathlib from the vs code extension, and get the same error when opening 00_first_proofs.lean in the tutorials directory; it runs for a while then times out. The leanproject binary doesn't seem to be included in .elan/bin so I can't download a cache.

[Patrick Massot]

You need to follow installation instructions from https://leanprover-community.github.io/get_started.html#regular-install if you want the full tooling

[Andrew Helwer]

(deleted)