[Documentation] When is it safe to have two processes spawn a `LeanREPLConfig` concurrently?

[jonathan-laurent]

When using LeanInteract with multiprocessing, the documentation clearly recommends to create a single LeanREPLConfig in the main process and then send it to worker processes that each spawn LeanServer instances from it. However, the question remains: is it unsafe to create two LeanREPLConfig instances in separate processes concurrently, and if so, are there specific cases where it is safe?

Indeed, there are clear use cases for creating configurations concurrently. For examples, one or several users might run several experiments concurrently, each via a Python script that uses multiprocessing. Can such cases present a risk? I imagine there is no risk when the configurations load projects from disjoint repositories. What if the same repository is used though? What if auto_build is set to True/False?

Answering such questions in the documentation would be valuable.

[augustepoiroux]

Good point, I will try to update the documentation soon.
In short, it is safe to create two, or more, LeanREPLConfig, LocalProject, GitProject, ... concurrently thanks to file locks. However, it is rather basic and other processes attempting to create the same config / project will wait.
If disk space is not a concern, for true parallelization, you can set the cache_dir parameter from LeanREPLConfig with a different directory for each process (works for LeanREPLConfig and GitProject, but not LocalProject where the copies should instead be made manually). This will make sure that each process is setting up its own directory / cache, not interferring with the other processes.

[jonathan-laurent]

Thanks for your answer. What parallelism opportunity is forfeited by not having separate caches exactly? Is it the case that building the project and accessing the incremental elaboration caches requires synchronization (but are one-time costs or relatively cheap anyway?) but calls to LeanServer.run can still run in parallel?

[augustepoiroux]

What parallelism opportunity is forfeited by not having separate caches exactly?

None

Is it the case that building the project and accessing the incremental elaboration caches requires synchronization (but are one-time costs or relatively cheap anyway?)

Building project and caching REPL version are one-time costs cached on disk. Once done, LeanServer.run can be run in parallel without any problem.
Incremental elaboration cache is in-memory cache and is tied to each LeanServer instance separately. It is possible to "synchronize" them between AutoLeanServer instances by using session caches class like ReplaySessionCache. But this is a weak synchronization: each instance has to run the commands added to the session cache independently.