excessive memory consumption?

Stream: new members

[Kevin Lacker]

Hey, so when I start a new Lean project it works fine. But when I open a file in mathlib (using emacs + lean mode), it uses a lot of cpu for a while and then shows errors everywhere, saying "excessive memory consumption" on fairly innocent lines like "import tactic.ring". Is this a known issue of some sort?

[Bryan Gin-ge Chen]

This indicates that your editor is forcing a recompile of mathlib, meaning that the oleans you have are out of date or out of sync with the Lean / mathlib version you're trying to use. It should be fixable by running leanproject get-mathlib-cache (if you're working on a project depending on mathlib) or leanproject get-cache (if you're working on mathlib itself).

[Kevin Lacker]

$ leanproject get-cache
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/106f3b54f790242fc8367d8337c371cfe70e73fe.tar.xz to /home/lacker/.mathlib/106f3b54f790242fc8367d8337c371cfe70e73fe.tar.xz
Trying to download https://oleanstorage.azureedge.net/mathlib/106f3b54f790242fc8367d8337c371cfe70e73fe.tar.gz to /home/lacker/.mathlib/106f3b54f790242fc8367d8337c371cfe70e73fe.tar.gz
Trying to download https://oleanstorage.azureedge.net/mathlib/106f3b54f790242fc8367d8337c371cfe70e73fe.tar.bz2 to /home/lacker/.mathlib/106f3b54f790242fc8367d8337c371cfe70e73fe.tar.bz2
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
Failed to fetch mathlib oleans

[Kevin Lacker]

is this related to that branch thing? i forked mathlib and made a change in my own branch

[Kevin Lacker]

does that break the build tooling

[Bryan Gin-ge Chen]

Ah, I see. That's a commit for your PR #4261. If you'd opened this PR from a branch inside mathlib then the CI would have created olean files that you could download with leanproject get-cache.

You might try leanproject build, but be warned this may take a while (30+ mins).

[Kevin Lacker]

leanproject build it is

[Bryan Gin-ge Chen]

A quicker way is to switch to current master, run leanproject get-cache, then rebase your branch on top of master.

[Kevin Lacker]

what would the rebase be doing there

[Kevin Lacker]

i mean, it's already on master, just the master branch of the fork

[Kevin Lacker]

are the cached oleans based on git hash?

[Bryan Gin-ge Chen]

Yes, they are.

[Kevin Lacker]

is there one generated for every master git hash or jsut every once in a while

[Bryan Gin-ge Chen]

One for every commit to every branch in the mathlib repo.

[Bryan Gin-ge Chen]

Although caches for non-head commits on non-master branches are removed after 3 days I think.

[Kevin Lacker]

ok then hopefully i should be able to checkout a previous hash, get-cache, and go back to the fork's master without altering the git tree

[Bryan Gin-ge Chen]

Yes, hopefully that should work too.

[Kevin Lacker]

looks like it works, thanks for the help!

[Kevin Lacker]

for subsequent mathlib PR's i'll use a branch on the mathlib repo itself