FrederickPu
FrederickPu
if we want tail recursion, can't we just put loop at the start
> **The memory of unused variable will not release anyway in repl, that's the biggest problem!** > > A more direct way to see what happes in repl: > >...
> Hi all, > > I find the way to implement tail recursion to replace repl loop, just modify two function definitions (`recordCommandSnapshot`, `repl`) in Main.lean as follows: > >...
what if we run the IO.processCommands on a different thread using IO.asTask?
we also want to avoid saving the proofSnapshots too
> 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: >...
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
In the following example ``` { "cmd": "import Mathlib" } {"env": 0} { "cmd": "theorem womp : 2 + 2 = 4 := sorry", "env": 1} { "sorries" : [...
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...