Excessive memory consumption for processing simple file.

[gruhn]

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

If I pass the following simple file to Lean, it seems to allocate unbounded amount of memory. I have to kill the process before my system freezes:

def digitsOf (num: Nat): List Nat :=
  let digit := num.mod 10
  let num_rest := num / 10 
  if num_rest == 0 then
    [digit]
  else
    have : num_rest < num := sorry
    digit :: digitsOf num_rest

example : digitsOf 1234 = [4,3,2,1] := by rfl

The function digitsOf is supposed to return a list of digits given some number. The problem seems to be the example. In particular, the by rfl proof. Without it, memory use stays below 300MB on my machine.

Screencast.from.2024-09-12.14-58-59.webm

If I use the CLI flag to limit memory use, I get the following output:

➜  lean-bug-demo lean --memory=300 digits.lean 
digits.lean:2:4: warning: declaration uses 'sorry'
digits.lean:2:4: warning: declaration uses 'sorry'
digits.lean:2:4: warning: declaration uses 'sorry'
digits.lean:11:42: error: The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
⊢ digitsOf 1234 = [4, 3, 2, 1]

But there is nothing wrong with the proof, right? I get the same output on live.lean-lang.org.

Steps to Reproduce

Create the lean file mentioned above and run lean the-file.lean.

Here is also a Dockerfile. With that, I can also reproduce the problem on Debian:

# Debian Bookworm base image
FROM buildpack-deps:bookworm

# download Lean 4.11.0 binary
RUN wget https://github.com/leanprover/lean4/releases/download/v4.11.0/lean-4.11.0-linux.zip 
RUN unzip lean-4.11.0-linux

# add the offending Lean file
COPY digits.lean /

To build the Docker image, make sure the digits.lean file is in the same directory. Then run:

docker build --tag demo .

To run lean inside Docker:

docker run --rm -it demo /lean-4.11.0-linux/bin/lean /digits.lean

On my machine memory use exploded. With or without Docker.

Versions

Tested both Lean 4.9.0 and Lean 4.11.0.

Tested on both NixOS 24.11 (Vicuna) and Debian Bookworm 12.7.

Impact

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

[nomeata]

Thanks for the report, and going through the lengths of making it reproducible, even with a docker image.

It looks like you are trying to reduce a function defined by well-founded recursion. This usually fails, even for small examples like this one, so this is probably a duplicate of #2171.

Note that since from Lean 4.12 on (#3772) rfl will reliably adhere to the irreducible flag on this definition, and fail properly.

[gruhn]

Thanks for the quick response. Not sure what that means. I'm quite a Lean beginner. So do you mean 4.12.0 would also resolve the memory issue?

For more context: I was just typing in my editor and then my system would totally freeze suddenly. Turns out the lean process spawned by the language server was consuming so much memory. I froze my system 2 or 3 more times before I manged to figure out where the problem was coming from.

Can you recommend some reasonable default memory limit?

[nomeata]

So do you mean 4.12.0 would also resolve the memory issue?

Yes, with it you shouldn’t be able to trigger the freeze here.

That said, presumably there might be other ways to freeze it up like this, and that’s certainly an issue. I don’t know if it’s a known one. Leaving open for the triage team to look at it in due course.

And with 4.12 the above proof won’t go by rfl anymore (because digitsOf will not reduce in the kernel; it’s not “definitionally equal”), but for example by simp [digitsOf] works.