6.5. Lean-Only Build🔗

If you only need to typecheck and build the Lean library, proofs, and test executables — without the FFI shim or any Rust output — the unmodified Lake invocation works on its own:

lake build

This is also what the top-level CMake driver invokes internally as its first step.