rw causes excessive memory consumption

Stream: general

[Kevin Buzzard]

Mathlib's ring_theory.perfection is slow. In fact I literally cannot compile it on one of my my machines -- if I am on master and I open src/ring_theory/perfection.lean and restart Lean then there is every chance I get excessive memory consumption errors. Can anyone else reproduce this? The reason we don't notice is that mathlib comes with its own olean files so we don't ever need to compile it (unless we're working on it). Even worse, if I am editing this file then the excessive memory consumption errors begin to show up more and more often, until eventually I get just into some situation where e.g. the orange bars never go away and I have to restart VS Code.

I would like to know the reason for this excessive memory consumption, and I can't figure it out. I have however spent several hours on this today, and have made some progress: I've managed to isolate what I think must be the issue, and furthermore I've made it mathlib-free (this is what took most of the time; I have no idea whether it's useful but it was certainly interesting). The issue is that there are sometimes goals of the form p f = q f and mathlib has a lemma foo of the form \forall t, p t = q t but rw foo takes a very long time to decide that t = f is a good idea. If you replace rw foo with rw foo f then this saves about 1.5 to 2 seconds of time on my machine for every rewrite, and can stop Lean going over the edge into the excessive memory consumption. The reason this is a problem is that a generic user would not know to do this, because rw foo should in theory just work fine.

Someone who is a master of Lean traces might be able to work out what wrong turn rw is taking, and the fix might be as simple as making something irreducible; if we could isolate this problem then it would lead to perhaps some nice speedup in this part of the library.

Here is an example using mathlib where we can see the problem. I am simply reproving some lemmas in ring_theory.perfection, using the rewrites with and without an explicit f.

import ring_theory.perfection

universe u

set_option profiler true
-- elaboration of pth_root_frobenius_quick took 114ms
lemma pth_root_frobenius_quick {R : Type u} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)]
  [char_p R p] : (perfection.pth_root R p).comp (frobenius _ p) = ring_hom.id _ :=
ring_hom.ext $ λ f, perfection.ext $ λ n, begin
  rw [ring_hom.comp_apply, ring_hom.id_apply, perfection.coeff_pth_root],
  rw perfection.coeff_frobenius f --
end

-- elaboration of pth_root_frobenius_slow took 2.92s
lemma pth_root_frobenius_slow {R : Type u} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)]
  [char_p R p] : (perfection.pth_root R p).comp (frobenius _ p) = ring_hom.id _ :=
ring_hom.ext $ λ f, perfection.ext $ λ n, begin
  rw [ring_hom.comp_apply, ring_hom.id_apply, perfection.coeff_pth_root],
  -- ⊢ ⇑(perfection.coeff R p (n + 1)) (⇑(frobenius ↥(ring.perfection R p) p) x) = ⇑(perfection.coeff R p n) x
  -- the LHS of the goal literally matches the LHS of the lemma.
  rw perfection.coeff_frobenius -- no f, costs us 1.5 seconds
end

-- elaboration of frobenius_pth_root_quick took 455ms
lemma frobenius_pth_root_quick {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
  (frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p) :=
ring_hom.ext $ λ f, perfection.ext $ λ n,
begin
  rw ring_hom.comp_apply,
  rw ring_hom.id_apply,
  rw ring_hom.map_frobenius,
  rw perfection.coeff_pth_root f,
  rw ← ring_hom.map_frobenius,
  rw perfection.coeff_frobenius f,
end

-- elaboration of frobenius_pth_root_slow took 16.2s
lemma frobenius_pth_root_slow {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
  (frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p) :=
ring_hom.ext $ λ f, perfection.ext $ λ n,
begin
  rw ring_hom.comp_apply,
  rw ring_hom.id_apply,
  rw ring_hom.map_frobenius,
  rw perfection.coeff_pth_root, -- no f
  rw ← ring_hom.map_frobenius,
  rw perfection.coeff_frobenius, -- no f
end

-- edit this comment a few times and you'll be in trouble
lemma I_can_break_lean {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
  (frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p) :=
ring_hom.ext $ λ f, perfection.ext $ λ n,
begin
  rw ring_hom.comp_apply,
  rw ring_hom.id_apply,
  rw ring_hom.map_frobenius,
  rw perfection.coeff_pth_root, -- no f
  rw ← perfection.coeff_pth_root, -- no f
  rw perfection.coeff_pth_root, -- no f
  rw ← perfection.coeff_pth_root, -- no f
  rw perfection.coeff_pth_root, -- no f
  rw ← perfection.coeff_pth_root, -- no f
  rw perfection.coeff_pth_root, -- no f
  rw ← perfection.coeff_pth_root, -- no f
  rw perfection.coeff_pth_root, -- no f
  rw ← perfection.coeff_pth_root, -- no f
  rw perfection.coeff_pth_root, -- no f
  rw ← perfection.coeff_pth_root, -- no f
  sorry
end
/-
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
-/

Here's an exercise: try and change the comments above the lemmas to the amount of time it takes to elaborate them on your machine. This will force Lean to compile and recompile the file, and eventually you will get an excessive memory consumption error, even if you were lucky enough to get the file to compile the first time around, as sometimes happens for me (especially if I restart VS Code -- then I am very likely to get it to compile the first time around). Just adding random comments to the file and then removing them will soon get you into trouble though, and then you get more and more excessive memory consumption errors and then you restart Lean and get more and restart Lean and get more and eventually have to restart VS Code again.

I have no idea whether not having mathlib as a dependency makes it easier to debug this issues, but here is a mathlib-free version, where I literally copied everything over, keeping the data but sorrying the lemmas. If I open this in a fresh file and then I just add random -- hi comments then it's not long before I get excessive memory consumption errors.(this is not true -- I had other mathlib files open including the bad one)

[Sebastien Gouezel]

Should ring.perfection be irreducible? Its definition is

/-- The perfection of a ring `R` with characteristic `p`,
defined to be the projective limit of `R` using the Frobenius maps `R → R`
indexed by the natural numbers, implemented as `{ f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }`. -/
def ring.perfection (R : Type u₁) [comm_semiring R]
  (p : ℕ) [hp : fact p.prime] [char_p R p] :
  subsemiring (ℕ → R) :=
{ zero_mem' := λ n, zero_pow $ hp.1.pos,
  add_mem' := λ f g hf hg n, (frobenius_add R p _ _).trans $ congr_arg2 _ (hf n) (hg n),
  .. monoid.perfection R p }

so if the docstring is correct the precise representation one uses is an implementation detail, and one should probably hide it. Also, with this definition (as a subsemiring), you see everywhere f: ↥(ring.perfection R p), with this weird arrow that is certainly making things complicated.

[Sebastien Gouezel]

subsemirings are important when you want to compare properties of the subring with the properties of the ambient ring. Here, I am not sure this really matters, right?

[Kevin Buzzard]

@Kenny Lau why do you keep it as a subring?

[Sebastien Gouezel]

Just as an experiment, I replaced the subsemiring by a type synonym (without making anything irreducible), just to remove the coe_to_sort. It's in branch#test_perfection. @Kevin Buzzard , could you check if it makes things better from your point of view, or if it doesn't change anything?

[Sebastien Gouezel]

I have made one further adjustment, and now everything seems to be instantaneous.

[Sebastien Gouezel]

#7583

[Patrick Massot]

It would be really nice to be able to extract reusable and teachable wisdom from such adventures.

[Kevin Buzzard]

This is why I made an effort to minimise -- I haven't looked yet but it sounds like Sebastien fixed the problem -- but there is some underlying rule here which I still haven't quite understood. Those rewrites look completely innocent.

[Sebastien Gouezel]

The type was too complicated so Lean got lost (coercions are complicated -- that's why they're gone in Lean 4, by the way). So I removed all the coercions and went back to plain subtypes. Can you confirm it works for you?

[Eric Rodriguez]

how are coercions being replaced in lean4?

[Eric Wieser]

Does yury's has_coe_to_sort refactor make this less bad?

[Kevin Buzzard]

Coercions to sort are gone in Lean 4? How do I promote a subring to a ring?

[Oliver Nash]

I guess this will be possible by manually invoking subtype?

[Oliver Nash]

As in:

variables (X : Type u) [ring X] (Y : subring X)

#check subtype Y.carrier -- `Type u`

example : ring (subtype Y.carrier) := Y.to_ring

[Mac]

Kevin Buzzard said:

Coercions to sort are gone in Lean 4? How do I promote a subring to a ring?

CoeSort is still around https://github.com/leanprover/lean4/blob/1e6dadfa5214b0fa2d6edb1494b7eb94accd4b15/src/Init/Coe.lean#L40-L41

[Mario Carneiro]

Coercions in lean 4 work differently, they no longer stick coe functions in the term. But they are still inferred using typeclasses the same way as lean 3

[Kevin Buzzard]

Were it not for all the old_structure stuff one would be able to easily port my example to Lean 4 and see if the problem remained.

[Eric Wieser]

That shouldn't be insurmountable, I think you've still done the majority of the really hard work there