Lean server keeps consuming more memory as it reprocesses a large definition

[pandaman64]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When interacting with a Lean server through VSCode and editing mid-file, the server often reprocess the definition later in the file. When a definition later in the file has many arguments with complex types, the server process consumes additional 1-2GB of RAM as it reprocess the definition, and it doesn't free the memory until my WSL environment crashes.

When setting LEAN_NUM_THREADS=1, the server still consumes additional memory, but the total memory usage of the server process will be capped at some point.

Context

This was originally reported at Zulip. The problematic definition is a custom induction principle that has 9 branches, and each branch takes 5-10 arguments.

Steps to Reproduce

I tried hard to minimize the issue, but it was difficult since commenting out parts of the definition reduces the additional memory usage significantly (often by an order of magnitude). At least the following code reproduces the issue without any dependencies in my environment.

Reproduction code

import Std.Data.HashSet

set_option autoImplicit false

open String (Pos Iterator)
open Std (HashSet)

#eval Lean.versionString -- "4.16.0-nightly-2025-01-23"

inductive Node where
  | done
  | fail
  | epsilon (next : Nat)
  | char (c : Char) (next : Nat)
  | split (next₁ next₂ : Nat)
  | save (offset : Nat) (next : Nat)
  | sparse (cs : Char) (next : Nat)
deriving Repr

structure NFA where
  nodes : Array Node
  start : Nat
deriving Repr

def get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Node :=
  nfa.nodes[i]

instance : GetElem NFA Nat Node (fun nfa i => i < nfa.nodes.size) where
  getElem nfa i h := get nfa i h

structure SearchState' (nfa : NFA) where
  states : HashSet (Fin nfa.nodes.size)
  updates : Vector (List (Nat × Pos)) nfa.nodes.size

abbrev εStack' (nfa : NFA) := List (List (Nat × Pos) × Fin nfa.nodes.size)

-- Run `top` and press Shift + M to see most memory-consuming processes.
-- Editing this comment will cause Lean server to re-check `εClosure'.induct'`,
-- leading to additional 1-2GB of memory consumption.
-- Don't forget monitoring the memory usage and restart the server before your system hangs with high memory pressure :)
theorem εClosure'.induct' (nfa : NFA) (it : Iterator)
  (motive : Option (List (Nat × Pos)) → SearchState' nfa → εStack' nfa → Prop)
  (base : ∀ matched next, motive matched next [])
  (visited :
    ∀ matched next update state stack',
    state ∈ next.states →
    motive matched next stack' →
    motive matched next ((update, state) :: stack'))
  (epsilon : ∀ matched next update state stack' state',
    state ∉ next.states → nfa[state] = .epsilon state' →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' ((update, state') :: stack') →
    motive matched next ((update, state) :: stack'))
  (split : ∀ matched next update state stack' state₁ state₂,
    state ∉ next.states → nfa[state] = .split state₁ state₂ →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' ((update, state₁) :: (update, state₂) :: stack') →
    motive matched next ((update, state) :: stack'))
  (save : ∀ matched next update state stack' offset state',
    state ∉ next.states → nfa[state] = .save offset state' →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' ((update ++ [(offset, it.pos)], state') :: stack') →
    motive matched next ((update, state) :: stack'))
  (done : ∀ matched next update state stack',
    state ∉ next.states → nfa[state] = .done →
    let next' := ⟨next.states.insert state, next.updates.set state update⟩;
    motive (matched <|> .some update) next' stack' →
    motive matched next ((update, state) :: stack'))
  (char : ∀ matched next update state stack' c (state' : Fin nfa.nodes.size),
    state ∉ next.states → nfa[state] = .char c state' →
    let next' := ⟨next.states.insert state, next.updates.set state update⟩;
    motive matched next' stack' →
    motive matched next ((update, state) :: stack'))
  (sparse : ∀ matched next update state stack' cs (state' : Fin nfa.nodes.size),
    state ∉ next.states → nfa[state] = .sparse cs state' →
    let next' := ⟨next.states.insert state, next.updates.set state update⟩;
    motive matched next' stack' →
    motive matched next ((update, state) :: stack'))
  (fail : ∀ matched next update state stack',
    state ∉ next.states → nfa[state] = .fail →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' stack' →
    motive matched next ((update, state) :: stack')) :
  ∀ matched next stack, motive matched next stack := sorry

1. Run top and press Shift + M to monitor the most memory-consuming processes
2. Copy the reproduction code in VSCode and watch the memory usage

• You can find the server process with ps aux | grep lean

3. Edit comments above εClosure'.induct' and watch Lean reprocess εClosure'.induct'
4. Look at the memory usage

Expected behavior: [Clear and concise description of what you expect to happen]

Reprocessing εClosure'.induct' shouldn't increase the memory usage of the Lean server process significantly.

Actual behavior: [Clear and concise description of what actually happens]

Reprocessing εClosure'.induct' causes the Lean server process to consume additional 1-2GB of RAM.

Versions

Lean: "4.16.0-nightly-2025-01-23"
OS: Ubuntu 22.04.4 LTS in WSL2 (5.15.167.4-microsoft-standard-WSL2)

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kim-em]

I can reproduce (on macos). For me it is not quite as much memory per edit (maybe 500mb on average? it's not uniform), and it seems to max out at around 15gb total memory.

[kim-em]

No difference in behaviour with set_option Elab.async false.

[pandaman64]

it seems to max out at around 15gb total memory

Yeah, the memory usage maxed out for me around 14-15GB if I assigned more RAM to WSL. By default, WSL can use at most 50% of the host Windows RAM (which is "only" 16GB for me), so consuming 15GB easily leads to halting the WSL environment (considering other Lean server processes also takes non-trivial amount of memory).