Zulip Chat Archive

Stream: general

Topic: Lean server blows up when adding a lemma to different file


view this post on Zulip Chase Meadors (Jan 23 2021 at 19:19):

So, I'm working on a copy of mathlib, on a branch that corresponds to a PR, so I can run leanproject get-mathlib-cache to get updated oleans for the tip of that branch.
I'm working in file 1, writing a theorem. Everything works great. Then, I go to file 2 to write a lemma I plan on using. After adding the lemma to file 2 and saving, upon returning to file 1, the lean infoview gets stuck on "Loading..." forever until it runs out of memory. It seems the trigger for this is simply trying to work in file 1 after changing/adding contents to file 2 (I haven't even referenced the new lemma in file 1 or anything yet).

I suspect maybe I need to rebuild/recompile file 2, but when I run "leanproject build" I think it tries to build everything, which happens to slam my CPU and slowly consume all of the memory on my machine, so I think maybe I'm doing something wrong :sweat_smile:

Can anyone help me out?

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:28):

which file is file 2?

view this post on Zulip Patrick Massot (Jan 23 2021 at 19:28):

We can't help you without any information about the import structure here.

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:28):

logic/basic.lean by chance?

view this post on Zulip Chase Meadors (Jan 23 2021 at 19:28):

In this case file one is ring_theory/noetherian.lean and file 2 is data/finset/lattice.lean

view this post on Zulip Patrick Massot (Jan 23 2021 at 19:29):

That's almost as good as logic/basic :lol:

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:29):

that will cause lots of rebuilding

view this post on Zulip Chase Meadors (Jan 23 2021 at 19:29):

Yeah, ok, that's what I suspected.

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:29):

if you want to save time, and not rebuild everything, but only the critical path to noetherian.lean, you can run

lean --make src/ring_theory/noetherian.lean

view this post on Zulip Johan Commelin (Jan 23 2021 at 19:30):

and get yourself a nice cup of tea (-;

view this post on Zulip Patrick Massot (Jan 23 2021 at 19:30):

The actual answer is you shouldn't edit such a low-level file until you are ready to either rebuild all of mathlib or push to GitHub to let GitHub do it for you.

view this post on Zulip Chase Meadors (Jan 23 2021 at 19:31):

I see. I believe the last time (before I knew about get-mathlib-cache) I tried to do leanproject build in mathlib, it consumed all 16 GB of RAM on my machine and slammed the CPU until the whole OS was locked up.

view this post on Zulip Chase Meadors (Jan 23 2021 at 19:32):

So, perhaps I'll just keep the lemma in file 1 for now until I would be ready to push to Github.

view this post on Zulip Bryan Gin-ge Chen (Jan 23 2021 at 19:42):

Note that it's totally fine to push commits to GitHub just to have their servers build mathlib instead of your own PC (and a lot of us do so). All PRs are squashed before merging into master so you don't have to worry about screwing up the commit history. Just keep in mind that GitHub Actions imposes some limits on the number of concurrent jobs, so try not to trigger more than say 10 jobs within 1-2 hours.


Last updated: May 12 2021 at 23:13 UTC