REPL garbage collection or fast pickleload

Stream: general

[Jiaming Shan]

Ok, so here is the question:
I am using LeanInteract (which is a REPL wrapper). I'm using ProofStep to search possible solution of a given sorry. However, it seems that ProofStep cannot do garbage collection (I mean after I try some possible solution and find I try too much and take too much memory, I want to remove some previously tried ProofStep, but I cannot find this feature) [method 1] [issues: clear memory, gc, LeanInteract)]. Another method is to restart the REPL instance and pickle load the sorry state, but it seems that pickle load need to reload Mathlib because of it's design, so the unpickle is slow (3s, which I expect 0.01s) [method 2] [issues: fast pickle, fork sorry state]. The implementation of AutoLeanServer add_to_session_cache in LeanInteract also relies on pickling, so it doesn't solve the issue.
What's the best way to do this?

[Auguste Poiroux]

Hi @Jiaming Shan!
If you are interested in the garbage collection feature, you can try out @RexWang PR. Since you are using LeanInteract, with >=0.6.0, you can:

1. Switch the REPL backend to his fork:

config = LeanREPLConfig(
    project=TempRequireProject("mathlib"),
    repl_git="https://github.com/Lean-zh/repl",
    repl_rev="gc-option",
)

2. Use run_dict method instead of the run method to use the newly introduced record parameter:

server.run_dict({"tactic": "linarith", "proofState": 0, "record": False})

Full example

# /// script
# dependencies = [
#     "lean-interact==0.6.0",
# ]
# ///
import time

import psutil

from lean_interact import Command, LeanREPLConfig, LeanServer, TempRequireProject
from lean_interact.utils import get_total_memory_usage

config = LeanREPLConfig(
    project=TempRequireProject("mathlib"),
    repl_git="https://github.com/Lean-zh/repl",
    repl_rev="gc-option",
)

server = LeanServer(config)
init_command = server.run(Command(cmd="import Mathlib\n\nexample (a b c : Nat) : (a + b) + c = c + a + b := by sorry"))

n = 0
started = int(time.time())
last_update = started

while True:
    n += 1
    if last_update != int(time.time()):
        elapsed = int(time.time()) - started
        current_memory = get_total_memory_usage(psutil.Process(server._proc.pid)) / 1024 / 1024
        print(
            f"{elapsed} seconds elapsed\t{n} issued commands\t{n // elapsed} commands/second\tMemory usage: {current_memory:.2f} MB"
        )
        last_update = int(time.time())
    response = server.run_dict({"tactic": "linarith", "proofState": 0, "record": False})

[Jiaming Shan]

Thank you! It's good, however my need is to remove previous ProofState, so something like "remove state" is more preferred. This idea is already mentioned in that issue, but I think it is not implemented right?

[Auguste Poiroux]

Oh, I see, sorry for the misunderstanding. Indeed, it would be an interesting feature to add. Regarding the behavior of the "delete proofstate" command, since we have a proof state tree, there is the question of the default behavior.
For example, let's say we have proof states 0 and 1, with 1 instantiated from 0. If we wish to delete 0, would you expect it to delete the whole associated subtree (i.e. 0 and 1 here)? or just 0?
I guess deleting only the specific proof state would be the default since proof states are independent once created.

[Jiaming Shan]

As you said, I would like to only delete 0 and keep 1 in the memory.

[Auguste Poiroux]

I guess it should be doable by replacing this line: proofStates : Array ProofSnapshot := #[] to proofStates : Array (Option ProofSnapshot) := #[], adding a new "remove" command which basically replaces the proof snapshot by None, and updating all the methods to handle this option change gracefully.
I don't have the bandwidth to implement that at the moment though, but maybe you can try to do it?

[Jiaming Shan]

Oh I see, that is useful! Thanks!

[Jiaming Shan]

So I do it myself and made a PR https://github.com/leanprover-community/repl/pull/111

[Auguste Poiroux]

Nice! Did you run tests to check if it is indeed releasing the memory associated to the removed proof states?

[Jiaming Shan]

I connect repl with state removing with LeanInteract, and test on LeanInteract to see the memory usage. It works! Although the memory that has been applied for will not be released, but if I release some proof states while continuously increasing the proof state, the program will not apply for new memory, thereby effectively curbing the growth of total memory.