FrederickPu

I don't think that's the issue cause when I run with `lake env` i get the `libc++abi` error again

I was able to get it working by using `Lean.loadDynlib` in the `runCommand function` https://github.com/FrederickPu/repl/blob/595d86879967f7cb0b982ad5436662783ac375a1/REPL/Main.lean#L296 I think the repl doesn't currently support taking Dynlib's as arguments

Should we add a dynlib command line option for lean repl? We've had similar issues come up when trying to use it for LeanEuclid

I've done the changes here: https://github.com/leanprover-community/repl/pull/124/files. I'm not sure how to write a test for it tho do we add canonical or leansmt to the test folder kinda like we...

The tests would prob only work one platform (eg linux is .so windows is .dll and make is .dynlib). So we might need a cmakelists too

We can do something like this ```cmake cmake_minimum_required(VERSION 3.10) project(mylib C) set(CMAKE_C_STANDARD 11) # Set library output directory set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) # Create shared library add_library(mylib SHARED mylib.c) # Set proper...

see README.md for more details about all of the available config options for batch commands

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

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...

> 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...