Lean takes all computer memory

Stream: general

[Antoine Chambert-Loir]

I'm in the midst of a small PR #11233, with a few modifications, but Lean is completely stuck, takes all the computer memory… What did I do wrong ?

[Antoine Chambert-Loir]

A ton of moving error messages such as
invalid import: data.option.defs excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)

[Yaël Dillies]

Your cache is messed up. Try getting a new one using leanproject get-cache and restarting the LEan server.

[Antoine Chambert-Loir]

Here is what happens :

(19:03) pro-acl > leanproject get-cache
Looking for mathlib oleans for eb0a06df7
  locally...
  remotely...
No cache available for revision eb0a06df7
Looking for mathlib oleans for 584c7bb0f
  locally...
  Found local mathlib oleans
No cache was available for eb0a06df7. A cache was found for the ancestor 584c7bb0f.
To see the intermediate commits, run:
  git log --graph eb0a06df7 584c7bb0f^!
Run `leanproject get-cache --rev` on one of the available commits above.
Failed to fetch cached oleans

:cry:

If I give leanproject the tag of the earlier revision, what will happen of my tiny modifications ?

[Yaël Dillies]

Supposedly nothing, but if you are on an old version of leanproject it might accidentally throw them away

[Yaël Dillies]

By that I mean it only fetches the cache. It doesn't do any git stuff.

[Johan Commelin]

@Antoine Chambert-Loir When in doubt, make sure that you save all your open files, and commit them.

[Arthur Paulino]

@Antoine Chambert-Loir You can try getting the cache from master and then merging master into your branch:

$ git checkout master
$ git pull origin master
$ leanproject get-cache
$ git checkout sign_from_cycle_type'
$ git merge master

[Alex J. Best]

Antoine Chambert-Loir said:

Here is what happens :

(19:03) pro-acl > leanproject get-cache
Looking for mathlib oleans for eb0a06df7
  locally...
  remotely...
No cache available for revision eb0a06df7
Looking for mathlib oleans for 584c7bb0f
  locally...
  Found local mathlib oleans
No cache was available for eb0a06df7. A cache was found for the ancestor 584c7bb0f.
To see the intermediate commits, run:
  git log --graph eb0a06df7 584c7bb0f^!
Run `leanproject get-cache --rev` on one of the available commits above.
Failed to fetch cached oleans

:cry:

If I give leanproject the tag of the earlier revision, what will happen of my tiny modifications ?

I'd try leanproject get-cache --fallback=download-all and see if that helps. It should be completely safe by now

[Junyan Xu]

Tiny changes may require many files be recompiled, so could be the cause of the problem. If that's the case, getting cache for an ancester version won't help. I suggest running leanproject build, or you may commit, push, wait for modified mathlib to be built/compiled on the cloud, leanproject get-cache when they are ready, then restart the server.

[Antoine Chambert-Loir]

This is certainly what happens, because I can't manage to have it work.
I tried a leanproject build but it was not finished 2 hours later…
Let's commit and push and check tomorrow!

[Adam Topaz]

@Antoine Chambert-Loir if you want to compile only the files necessary for a single lean file called foo.lean, you can use lean --make foo.lean. If you instead use leanproject build, it will try to build the whole library.

[Adam Topaz]

So, if you're editing some file a.lean that is imported by many other files, and you next want to work on b.lean which imports a.lean, if you use lean --make b.lean, then only the bare minimum will be compiled..

[Martin Dvořák]

It seems that I run into similar problems in my PR https://github.com/leanprover-community/mathlib/pull/11181.

[Martin Dvořák]

https://github.com/leanprover-community/mathlib/pull/11181#issuecomment-1005956398

[Martin Dvořák]

Issue solved by letting GitHub build the project and getting olean from GitHub. VS code doesn't seem useable for building large Lean libraries.

[Eric Rodriguez]

if you want to build locally, you should use leanproject build

[Martin Dvořák]

I've done that twice. My computer ran overnight and finished it in late morning.