Lean-interact container cold start

Stream: lean4

[Manooshree Patel]

Hello! I'm working on an educational app, with a Lean verification component, that is being deployed on Google Cloud Run. We're using the lean-interact package for verifying Lean proofs. Right now, the Lean server initialization time is creating a very unpleasant user experience, as bringing up an instance of lean-interact can take from 3-7 minutes. I was wondering if there's any way we can bring down this cold-start time? I have attached a log after a first query is sent to the container as well as our docker file. I've also included our container specs.

Thank you in advance!

Screenshot 2026-01-21 at 6.45.49 PM.png
Dockerfile
Screenshot 2026-01-21 at 6.47.32 PM.png

[Snir Broshi]

Hello, by "lean-interact" are you referring to https://github.com/augustepoiroux/LeanInteract from #Machine Learning for Theorem Proving > REPL: automated incremental state reuse across commands @ 💬?

[Manooshree Patel]

yes!

[Snir Broshi]

Where is the log "Checking to make sure Mathlib is available (this serves to check if imports succeeded)..." coming from? It's not in lean itself, nor in LeanInteract, nor in the Dockerfile you shared. Is this from another part of your infra?

[Snir Broshi]

Ditto for "Starting the Lean Interact server..."

[Manooshree Patel]

Those logs come from initializing the LeanRunner in run_lean.py. I've attached that file, as well as the lean_compiler.py file, which contains the LeanCompiler class that is used throughout our app.

lean_compiler.py
run_lean.py

[Snir Broshi]

Can you create a #mwe, in this case perhaps a dockerfile that reproduces the problem exactly with no extra files? Debugging your python code is a bit out of scope for this forum