Zulip Chat Archive

Stream: general

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

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?

Johan Commelin (Jan 23 2021 at 19:28):

which file is file 2?

Patrick Massot (Jan 23 2021 at 19:28):

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

Johan Commelin (Jan 23 2021 at 19:28):

logic/basic.lean by chance?

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

Patrick Massot (Jan 23 2021 at 19:29):

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

Johan Commelin (Jan 23 2021 at 19:29):

that will cause lots of rebuilding

Chase Meadors (Jan 23 2021 at 19:29):

Yeah, ok, that's what I suspected.

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

Johan Commelin (Jan 23 2021 at 19:30):

and get yourself a nice cup of tea (-;

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.

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.

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.

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: Aug 03 2023 at 10:10 UTC