`server.run(lean_interact.Command(…))` starts failing after ~560 issued commands

[euprunin]

It seems like server.run(lean_interact.Command(…)) starts failing after ~560 issued commands.

The following code reproduces the issue consistently for me:

#!/usr/bin/env python3

import time

import lean_interact

if __name__ == "__main__":
    server = lean_interact.LeanServer(lean_interact.LeanREPLConfig())
    n = 0
    started = int(time.time())
    last_update = started
    while True:
        n += 1
        if last_update != int(time.time()):
            elapsed = int(time.time()) - started
            commands_per_second = n // elapsed
            print(
                f"{elapsed} seconds elapsed, {n} issued commands, {commands_per_second} commands/second"
            )
            last_update = int(time.time())
        response = server.run(lean_interact.Command(cmd=f"#check Nat"))
        assert response.messages
        assert response.messages[0].data == "Nat : Type"

Output:

59 seconds elapsed, 532 issued commands, 9 commands/second
60 seconds elapsed, 541 issued commands, 9 commands/second
61 seconds elapsed, 549 issued commands, 9 commands/second
62 seconds elapsed, 557 issued commands, 8 commands/second
Traceback (most recent call last):
…
    raise BrokenPipeError("The Lean server returned no output.")
BrokenPipeError: The Lean server returned no output.

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
…
    raise ConnectionAbortedError(
    ...<5 lines>...
    ) from e
ConnectionAbortedError: The Lean server closed unexpectedly. Possible reasons (not exhaustive):
- An uncaught exception in the Lean REPL (for example, an inexistent file has been requested)
- Not enough memory and/or compute available
- The cached Lean REPL is corrupted. In this case, clear the cache using the `clear-lean-cache` command.

Environment:

% python3 --version
Python 3.13.2
% sw_vers
ProductName:		macOS
ProductVersion:		15.1.1
BuildVersion:		24B2091

[augustepoiroux]

Hi,

This is indeed a known issue of the REPL (see leanprover-community/repl#77)
A few things about this:

• The server is running out of memory. This is because each command is stored in memory. A work in progress in the repl is adding an option to discard unused environments add garbage collection option leanprover-community/repl#83
• Commands not depending on previous commands (i.e. not setting the env attribute of Command) generally take more time to process and more memory because the environment has to be set up. In your code, if you run a first dummy command Command(cmd="#check Nat) before the loop, and then run the next commands in your iteration loop as follows Command(cmd=#check Nat", env=0) you will notice an important speed up. (note: however, imports should always be contained in the first command)
• Second, I recommend checking AutoLeanServer. It can be used in place of LeanServer. It will restart automatically once out of memory.

[augustepoiroux]

Hi, this issue should now be solved in the nightly branch ;)