Server mode

[vadimkantorov]

Hi!

In the recent Kimina-Prover paper is mentioned:

Lean Server. In our reinforcement learning and evaluation pipelines, we integrate the Numina Lean Server (Numina
2025) as the verification backend to provide real-time feedback for generated proof attempts. Built upon Lean FRO’s
LeanREPL (Lean FRO 2023), the Numina Lean Server employs an LRU-based caching mechanism that reuses
preloaded environments based on import headers, significantly reducing initialization overhead. Furthermore, it
supports extensive parallelization across multiple CPUs by managing multiple Lean REPL processes concurrently.
These innovations result in a 10× speedup in verification throughput, achieving up to 100 iterations per second on
machines equipped with 64 CPU cores and 512 GB RAM. 

Would you have an advise what they might mean by LeanRepl preloaded environments (based on imports)?

In effect, what would be the fastest way of initializing LeanRepl process instances, given some known imports?

E.g. is it possible to do some kind of forkserver and simply clone process once it's done loading the imports? Or is there another way of snapshotting the Lean REPL state and quickly loading / resetting to it?

For Lean-in-the-loop proof generators it's very important to have a lightning-fast LeanRepl server interface which can be deployed to a big machine and manage LeanRepl workers in the most efficient way (e.g. they should fast super-fast and maybe have a pre-ready pool of LeanRepl worker processes)?

[augustepoiroux]

My understanding is that they run the imports once, and then, using the environment state of the imports, they check the proofs. If you generate thousands of proofs for a single problem, this means that you load the imports only once in order to check all the proofs.
You can check my implementation of this here.

There is also the pickling feature of the REPL:

{"pickleTo": "path/to/file.olean", "env": 7}

{"pickleTo": "path/to/file.olean", "proofState": 17}

{"unpickleEnvFrom": "path/to/file.olean"}

{"unpickleProofStateFrom": "path/to/file.olean"}

However, I am not sure this is faster than just re-running the imports from scratch, given the way it is implemented. If you benchmark this, I am interested in the results :)
Anyway, I think importing Mathlib takes less than 5 seconds, so if you load all your different headers once at the beginning of your training, it should be fine.

[vadimkantorov]

Thanks for the response! Yes, will let know when I get any benchmarks!

Also, is LeanRepl process fork-safe? E.g. would it work if I fork the initial LeanRepl process after all the imports?

[RexWzh]

@augustepoiroux The pickling feature is not stable actually, see: #81

[augustepoiroux]

Indeed, I also reported another issue with pickling in #62. But I think there are no issues when pickling a command containing only imports.

[vadimkantorov]

Regarding pickling/unpickling:

Somehow import MathLib takes ~40 seconds on my machine, and unpickling an olean env with these imports takes as much. Is it expected?

Are there any ways to trace these imports? 40 seconds on my machine does not match at all 5 seconds on your machine, so I suspect something must be wrong on my machine

[augustepoiroux]

Are you using a HDD disk? Not sure, but this might explain the difference. Another potential explanation is if you have run lake exe cache get but not lake build in your project.
Can you try the following:

1. Run the {'cmd": "import Mathlib"} command multiple times. Does it always take ~40s?
2. In this project, how long does VSCode takes to process a file with just import Mathlib in it?

About unpickling, this is what I expected. The pickling feature does not save the environment state, but rather a way to replay it.

[vadimkantorov]

I'm using a networked SSD

1. Yes :(
2. I'll try it. I'm not connecting VS Code to this cloud machine yet

I did lake build, but not lake exe cache get. Should I also do lake exe cache get?

I get the same slow 40s, when I directly invoke lean binary without REPL, so it appears to be Lean's fault, not REPL's.

Is there any way to profile the imports?

[vadimkantorov]

Regarding REPL, for server mode, it might be interesting to have a forkserver mode, especially if lean itself is fork-safe? so that one can get fast a process which already has all imports done

[augustepoiroux]

Should I also do lake exe cache get?

If your project depends on Mathlib, lake exe cache get avoids having to recompile Mathlib yourself.

I don't know Lean enough to help you on the other questions. But I am interested in the answer if you find something.

[RexWzh]

They just released the code here: https://github.com/project-numina/kimina-lean-server

And the LRU-based caching mechanism :
https://github.com/project-numina/kimina-lean-server/blob/1d0c84e3e8a65ee0bb888f5f04b512c3a29dd08c/utils/repl_cache.py#L16-L29