Lean server blows up when adding a lemma to different file

Stream: general

[Chase Meadors]

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?

[Johan Commelin]

which file is file 2?

[Patrick Massot]

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

[Johan Commelin]

logic/basic.lean by chance?

[Chase Meadors]

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

[Patrick Massot]

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

[Johan Commelin]

that will cause lots of rebuilding

[Chase Meadors]

Yeah, ok, that's what I suspected.

[Johan Commelin]

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

[Johan Commelin]

and get yourself a nice cup of tea (-;

[Patrick Massot]

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.

[Chase Meadors]

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.

[Chase Meadors]

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

[Bryan Gin-ge Chen]

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.