leanprover-community
Add batch processing to LeanRepl
Able to process multiple commands at once using
{ "cmds": ["theorem womp : 2 + 2 = 4 := by rfl", "#eval 0 = 2"]}
Also added multithreading parallelism using Task monad as well as option to garbage collect command snapshots (this overlaps with https://github.com/leanprover-community/repl/pull/83.
Batch commands have timeouts to prevent one bad proof from stalling the batch which overlaps with https://github.com/leanprover-community/repl/pull/92. Timeouts are in milliseconds and can be set using an option
{ "cmds": ["theorem womp : 2 + 2 = 4 := by rfl", "#eval 0 = 2"], "timeout": 6000}
Right now, there is no command snapshotting for batch commands.
see README.md for more details about all of the available config options for batch commands
Amazing feature, thanks for sharing it! A few comments:
- There is a typo:
parrallel->parallel - I see you pushed some python code and text files for testing. I don't have a strong opinion on mixing the REPL with python code, but maybe not everyone would agree, just telling you in case ^^
the python code is just for benchmarking, I can get rid of it before we merge (and generate a corresponding .in file) before we merge
One useful option could also be something along the lines of "skip processing elements if an earlier example got verified okay". This can be useful for verifying multiple proofs for the same problem produced by whole-proof completeion LLMs (e.g. 32 or 256 or several thousand roll-outs). Sometimes we are already satisfied if we found a single proof and for time-saving, all further proofs of the given problem can be skipped
I agree this can be a useful feature. ~This can be implemented with IO.waitAny, and then cancelling the other jobs (hoping the jobs will cooperate though).~ Nevermind, it is not that straightforward as the first job to finish may fail.
i think to do this efficiently you would need to poll each pending task to see if it has yielded a successful result at regular intervals kind of like I do for the withTimeout function
This sounds like a good practical approach. I wonder if there is a more efficient way of doing this though.
For example, regarding timeout, I think I prefer the approach in https://github.com/leanprover-community/repl/pull/92. IO.waitAny is used to terminate as soon as the command or the timeout terminate instead of checking at regular intervals.
One useful option could also be something along the lines of "skip processing elements if an earlier example got verified okay".
It could also be good to process the batch in micro-batches (when configured) - so that the CPU utilization can be maximized. When I ran REPL, I got typically 10% utilization of a single CPU core. So bringing it up would be useful.
Another question is multi-core processing. Then maybe proofs should be annotated with problem-name, so that simultaneously multiple micro-batches from different problems can be processed
If you look at the readme file in this PR, I think @FrederickPu already implemented that through the "buckets" parameter
If you look at the readme file in this PR, I think @FrederickPu already implemented that through the
"buckets"parameter
When running in parallel mode on a VM with 300+ cores I max out at a 7x speedup. So I'm not sure if core level parallelism is being acheived