Zulip Chat Archive

Stream: new members

Topic: excessive memory consumption?


view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:04):

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?

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:11):

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).

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:12):

$ 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

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:13):

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

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:13):

does that break the build tooling

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:14):

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).

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:15):

leanproject build it is

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:16):

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

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:17):

what would the rebase be doing there

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:18):

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

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:19):

are the cached oleans based on git hash?

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:19):

Yes, they are.

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:19):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:20):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:21):

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

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:24):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 28 2020 at 17:24):

Yes, hopefully that should work too.

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:24):

looks like it works, thanks for the help!

view this post on Zulip Kevin Lacker (Sep 28 2020 at 17:25):

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


Last updated: May 18 2021 at 17:44 UTC