Lean keeps crashing when editing mathlib

Stream: new members

[Sebastian Monnet]

I'm trying to PR the following lemmas:

@[simps] def ring_equiv.subsemiring_equiv_map {A B : Type*} [non_assoc_semiring A]
  [non_assoc_semiring B] (e : A ≃+* B) (R : subsemiring A) :
  R ≃+* R.map e.to_ring_hom :=
{ ..e.to_add_equiv.add_submonoid_equiv_map R.to_add_submonoid,
  ..e.to_mul_equiv.submonoid_equiv_map R.to_submonoid}

def ring_equiv.subring_equiv_map {A B : Type*} [ring A]
  [ring B] (e : A ≃+* B) (R : subring A) :
  R ≃+* R.map e.to_ring_hom :=
e.subsemiring_equiv_map R.to_subsemiring

def alg_equiv.subalgebra_equiv_map {R A B : Type*} [comm_semiring R] [semiring A]
  [semiring B] [algebra R A] [algebra R B] (e : A ≃ₐ[R] B) (S : subalgebra R A) :
  S ≃ₐ[R] (S.map e.to_alg_hom) :=
{ commutes' := λ r, by { ext, simp },
  ..e.to_ring_equiv.subsemiring_equiv_map S.to_subsemiring,
}

def alg_equiv.intermediate_field_equiv_map {K L M : Type*} [field K] [field L] [field M]
  [algebra K L] [algebra K M] (e : L ≃ₐ[K] M) (E : intermediate_field K L) :
  E ≃ₐ[K] (E.map e.to_alg_hom) :=
e.subalgebra_equiv_map E.to_subalgebra

I got a clean copy of mathlib with leanproject get mathlib, and pasted the first lemma into ring_theory.subsemiring.basic.lean, removing ring_equiv from the name since I put it in the ring_equiv namespace. This worked fine and ring_theory.subsemiring.basic.lean still compiled. Without changing anything else, I then opened field_theory.intermediate_field.lean, and Lean immediately crashed with lots of errors of the excessive memory consumption detected at variety.

I've done this a few times with clean copies of mathlib, and the same thing happens every time. Does anyone have any idea what's going on?

[Arthur Paulino]

Try getting cached olean files with leanproject get-cache inside the mathlib directory. Building everything on your machine is very likely to consume all the memory you have available and still fail because you didn't have enough

[Eric Rodriguez]

yeah, i'd just push to CI and see where it fails. otherwise you can build locally but outside vscode with leanproject build, or you can increase your memory threshold in VSCode (although this is a bandaid)

[Sebastian Monnet]

leanproject get-cache doesn't seem to help. Is this a normal error? Alright, I'll just try making a PR anyway and hope for the best

[Kevin Buzzard]

If you edit a file near the root of the heirarchy then Lean can become unusable very quickly, because any olean files which you have lying around which depend in some way on this file are instantly irrelevant and all need to be recompiled. So the trick is to add the lemmas from the leaves up, although hmm that's not going to work in your case because each one needs the ones before!

[Arthur Paulino]

If you're editing a file near the root of the hierarchy, then make sure you don't have other (higher) files open because that would most likely trigger the recompilation Kevin mentioned

[Patrick Massot]

@Sebastian Monnet I'll teach you advanced leanproject magic so that you can see how gentle you are with your CPU:

leanproject import-graph --from ring_theory.subsemiring.basic --to field_theory.intermediate_field gra.pdf

[Patrick Massot]

The result is gra.pdf

[Patrick Massot]

That's everything Lean needs to compile when you access field_theory.intermediate_field after modifying ring_theory.subsemiring.basic

[Arthur Paulino]

I was in a similar situation just yesterday because I added three lemmas here (and modified one slightly).

My computer could handle it if I didn't open any other lean file, but then I wasn't able to see the impact of my changes on other files I was working on. So I ended up just pushing it and watching what the CI tests said :shrug:

[Patrick Massot]

And leanproject get-cache isn't doing magic, it's trying to fetch some compiled file that have been compiled elsewhere, by someone else's CPU. It doesn't instantly compile your stuff on your machine. You can indeed use it, but it won't save time. You can commit your change to the first file in some new git branch, push the branch to the mathlib repo (the official one, not a fork) and then wait for some other machine to compile. Then you'll be able to get the cache.

[Alex J. Best]

You can also call lean with the "--old" flag to help in these situations, though it does come with some caveats.
You can enable it by opening the vscode settings and searching for "Lean: extra options" then add the flag "--old".
This causes lean not to recompile oleans for unedited files and just assume everything worked, so in this situation it is helpful to avoid recompilation, but you do then run the risk that your change broke /changed the meaning of some file inbetween. Thus it most applicable when you are adding a new lemma/def early in the hierarchy that you are sure won't break things in between, rather than changing existing defs.
I normally run lean with this flag enabled and then disable it if I start getting weird error messages I don't understand.
Indeed I just checked and it is possible to "prove false" running lean with the old flag on, so really you should use with care.