FrederickPu

Results 49 comments of FrederickPu

Add batch processing to LeanRepl

Should we do thread level parallelism within each bucket?

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

But I wait for each cmd to finish before running the next one. Is there any way to clear away the memory allocation once the command is done being run?

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

also is there any way to check the current memeory usage from within leanrepl?

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

I made my own version of runCommand that doesn't save any enviroment data and I still get the same error: ``` import REPL open Lean Elab namespace REPL def runCommand'...

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

I wonder if we can piggy back off of some `Lake`'s scheduling system to do this more efficiently.

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

so is the idea that the headers are being generated faster than they can be garbage collected or smth?

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

what if you wait for 2 minutes or something. Does it still never get released?

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

can we escalate this to a lean language issue?

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

so is the issue that it's just garbage collecting them too slowly

LeanRepl terminates trying to run large amounts of commands on a single LeanRepl instance

do you have any idea which variable remains in scope beyond a single runCommand function?