add garbage collection option

[RexWzh]

Add a record option to optimize memory usage. The reference-counting issue is fixed by @ohyeat as discussed here.

[kim-em]

What is this meant to do? This needs documentation!

[RexWzh]

I just updated the readme. Setting gc = true will discard the environment after execution, useful for memory management.

[RexWzh]

The code modifications for unsafe def repl are written by @ohyeat , replacing loops with tail recursion.

I've tested these changes using statements from MiniF2F. Here are the test samples:

{"cmd": "import Mathlib\nopen BigOperators Real Nat Topology Rat"}

-- tactic mode
{"cmd": theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x :\n    ∀ x > 0, 2 - Real.sqrt 2 ≥ 2 - x - 1 / (2 * x) := by sorry", "env": 0}

-- command mode
{"cmd": "theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x :\n    ∀ x > 0, 2 - Real.sqrt 2 ≥ 2 - x - 1 / (2 * x) := by", "env": 0}

-- gc for tactic mode
{"cmd": "theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x :\n    ∀ x > 0, 2 - Real.sqrt 2 ≥ 2 - x - 1 / (2 * x) := by sorry", "env": 0, "gc": true}

-- gc for command mode
{"cmd": "theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x :\n    ∀ x > 0, 2 - Real.sqrt 2 ≥ 2 - x - 1 / (2 * x) := by", "env": 0, "gc": true}

And the test results:

[FrederickPu]

we also want to avoid saving the proofSnapshots too

[RexWzh]

The proofSnapshots are essential for tactic mode - without them, the proofState id would be invalid when running commands in the format {"tactic": "xxx", "proofState":xxx}.

ADD:

However, the command that creates the proofSnapshot can be garbage-collected. See the green and yellow lines in the diagram above. I will add more tests later.

[augustepoiroux]

Just a question of aesthetics. I would prefer the option to be called discardState instead of gc.
Or maybe we do the opposite and call this option recordState or saveState, with true as default value.
Don't know which option is better ^^

Other than that, I think this is a useful feature 👍

[RexWzh]

Just a question of aesthetics. I would prefer the option to be called discardState instead of gc. Or maybe we do the opposite and call this option recordState or saveState, with true as default value. Don't know which option is better ^^

Other than that, I think this is a useful feature 👍

You mean discardCmd, right?

As for discardState, I think implementing something like deleteState might be more plausible. We would rarely create a state and discard it immediately.

[FrederickPu]

The proofSnapshots are essential for tactic mode - without them, the proofState id would be invalid when running commands in the format {"tactic": "xxx", "proofState":xxx}.

ADD:

However, the command that creates the proofSnapshot can be garbage-collected. See the green and yellow lines in the diagram above. I will add more tests later.

The whole point of garbage collecting a command is that you never interact with its state again. So you won't apply tactics on its proof state

[RexWzh]

@augustepoiroux I think using discard would be sufficient since it only applies to command mode.

with true as default value

We'd better set false as default to be compatibile with previous versions. For example, users need to set discard=false when first running import Mathlib :)

[augustepoiroux]

Nice 👍 I agree with you about keeping backward compatibiliy. Regarding

with true as default value

The full sentence is

Or maybe we do the opposite and call this option recordState or saveState, with true as default value.

It is just a change of point of view. Instead of discarding commands, we record them. My naming was bad, but the idea was essentially to replace gc by record and inverting all the values. I.e. gc=True <-> record=False. And in this case we would have record=True as the default value, which keeps the current behavior of the REPL ;)

[RexWzh]

@FrederickPu

The proofSnapshots are stored in proofStates and can exist independently of their corresponding env commands.

repl/REPL/Main.lean

Lines 61 to 74 in 506a6f3

	/-- The monadic state for the Lean REPL. -/
	structure State where
	/--
	Environment snapshots after complete declarations.
	The user can run a declaration in a given environment using `{"cmd": "def f := 37", "env": 17}`.
	-/
	cmdStates : Array CommandSnapshot := #[]
	/--
	Proof states after individual tactics.
	The user can run a tactic in a given proof state using `{"tactic": "exact 42", "proofState": 5}`.
	Declarations with containing `sorry` record a proof state at each sorry,
	and report the numerical index for the recorded state at each sorry.
	-/
	proofStates : Array ProofSnapshot := #[]

For verification, you can check the test cases in this PR:

https://github.com/leanprover-community/repl/pull/83/files

[FrederickPu]

then there should be an option to discard proof states as well. For example if you are doing proof repair, then you don't every use the tactic thing

[RexWzh]

For example if you are doing proof repair, then you don't every use the tactic thing

@FrederickPu I've implemented similar command mode features for tactic mode and am currently testing how these features reduce memory usage.

Also, note that setting record=false will discard states created by tactics, but not states created by sorry. For example, tactics like have : 1=1 := by sorry will still create additional states.

btw, deleting goals could disrupt the proofState id, so we should avoid that approach.

The whole point of garbage collecting a command is that you never interact with its state again.

You can still interact with the state even after garbage collecting the command. This could address the issue you posted earlier.

[RexWzh]

@kim-em I think this PR is ready.

Setting record=False enables garbage collection of environment snapshots. This helps reduce memory usage from continuously increasing, although commands like {"cmd":"import xxx"} cannot be garbage collected.

Additionally, it can serve as a health check command. For example:
{"cmd":"#check true", "record":false} can be used to verify if the REPL is alive without modifying the environment snapshots.

Thanks for your time and effort for reviewing these changes.

[kim-em]

I don't understand here: if we're generating proofState: 0 here, and it is actually usable, then the environment has been transitively captured, and the record: false wasn't really respected.

[FrederickPu]

Rex said that you can garbage collect the command that created the proof snapshot without garbage collecting the proof snapshot itself. I'm not sure what the use case for this would be tho. Also I think having each proof snapshot connected to a command would make it easier to garbage collect all the snapshots after you are done with tactic mode for a particular problem.

[RexWzh]

You can check the green(garbage collected) and yellow lines in the diagram above. Here are the relevant commands:

# By default, this consumes about 83 MB
[{'cmd': 'import Mathlib'},
 {'cmd': 'theorem womp0 (a0 b c : Nat) : (a0 + b) + c = c + a0 + b := by sorry', 'env': 0},
 {'cmd': 'theorem womp1 (a1 b c : Nat) : (a1 + b) + c = c + a1 + b := by sorry', 'env': 0},
 # ...
]

# With record=False, this consumes about 21 MB
[{'cmd': 'import Mathlib'},
 {'cmd': 'theorem womp0 (a0 b c : Nat) : (a0 + b) + c = c + a0 + b := by sorry', 'env': 0, 'record': False},
 {'cmd': 'theorem womp1 (a1 b c : Nat) : (a1 + b) + c = c + a1 + b := by sorry', 'env': 0, 'record': False},
 # ...
]

The ProofSnapshot is independent of the cmdSnapshot once created. The structure provides sufficient information for interactions and pickles.

structure ProofSnapshot where
  coreState     : Core.State
  coreContext   : Core.Context
  metaState     : Meta.State
  metaContext   : Meta.Context
  termState     : Term.State
  termContext   : Term.Context
  tacticState   : Tactic.State
  tacticContext : Tactic.Context
  rootGoals     : List MVarId

[RexWzh]

and the record: false wasn't really respected

We can view it this way: in Cmd mode, record is intended for cmdSnapshot-gc, while in Tactic mode, it's for proofSnapshot.
And it can be used as default config for tactic-based interactions, as the generated cmdSnapshots are rarely used since they contain sorry.

If someone wishes to obtain the state while discarding both the cmdSnapshot and proofSnapshot, they can use the File mode like:

{"cmd": "example : 1 = 1 := by", "env": 0, "record": false}

And then extract the states from errors.

btw, this feature is beneficial for File-mode-based interactions like itp-interfaces, where most generated cmdStates are wasted due to incomplete errors.

[FrederickPu]

ahh so command snapshots are only necessary to create additional command states. Which rarely happens for a single proof. Like usually u would only want to snapshot import headers and stuff

[desaxce]

The code looks good, that's a nice feature, I don't see anything preventing the merge apart from refreshing the branch and tests.

[desaxce]

Can you please update your fork and update your branch to be on 4.22.0-rc3?
Then you can remove the "Goals accomplished!" below, it's not returned anymore.

[RexWzh]

Thanks for your review. I have merged the latest code and updated the test script.

=== Test Summary ===
Failed tests:
✗ record_cmd2
Total: 1 failed
==================

[desaxce]

@kim-em Do you think we could merge this development?
The new record parameter helps a lot limiting memory use on a REPL.

[augustepoiroux]

Can someone make a summary of what "record": false does exactly in each case?
From what I understood, if the command contains sorries, then the proof states are recorded, and the command state is transitively recorded as well, right?
Is there a way to not record a command state, regardless of whether it contains sorries?

[FrederickPu]

In the following example

{ "cmd": "import Mathlib" }
{"env": 0}
{ "cmd": "theorem womp : 2 + 2 = 4 := sorry", "env": 1}
{ "sorries" : [ {"proofState": 0, ....}] }

The proofState=0 is defined entirely in terms of the context env=0 so env=1 can be discarded entirely. I think that was @RexWzh 's idea. However, if the command for env=1 created new declarations I don't think this intuition would hold.

The only state that is transitively saved in the proofSnapshot is the Enviroment through Meta.Context or something like that. Ie all of the parsed information from the Command.json won't be included only the context necessary for creating the syntax of the tactic state for the proofsnapshot.

[FrederickPu]

I think it would be nice to have a way of discarding proofsnapshots once they are no longer being used. Ie you've finished with your proof search for a particular problem.