Docs How-to guides How-to guides Steps for one job at a time, for when you already know Lema and know what you want to do.
Each guide names a goal and gives the steps to reach it, with the commands and the refusals you may meet on the way. The guides assume you have worked through the tutorials or know the same ground. For exact flags and fields, see the reference .
Install the pinned Lean by hand Download Lean 4.34.1, check it against the committed pins and verify the extracted tree with lema verify-distribution. Write a runtime configuration Point native calls at the pinned Lean distribution, an owner-only output directory and a shared lock, with an optional call budget. Create a store with a narrower axiom policy Start a store that accepts only propext and Quot.sound, and read which axioms each accepted object uses. Move an alias safely Point a name at a new object without losing a concurrent change. Replace an implementation Move an implementation's alias to a new implementation, backed by an accepted proof that the new one replaces the old. Name a set of objects with a bundle Record a set of accepted objects under export names once, then receive them all in a draft as Received bindings. Set up a project reference Register actors, then move a project reference between revisions under a policy you choose. Report on a change and merge two lines Classify what a revision or reference move changes, then join two lines of revisions at their common base. Build static inspection pages Write plain HTML, Markdown and JSON pages of chosen references, releases and pending reviews from a store. Build a native executable Compile an execution manifest's accepted closure into a native executable linked by leanc, then run it in the sandbox. Release an artifact Pin a built artifact to the store's accepted closure and a deployment configuration, then run it by release ID. Build a capability app Build an app manifest against the capability platform, test it in a deployment and link a standalone binary. Re-check a store from scratch Replay accepted objects with the pinned Lean kernel and no cached modules, and compare every axiom footprint with its receipt. Recover from a HALTED latch Find out why native calls stopped, read the ledger and the faulted call's records, and clear what the runtime checks. Run the test suites Run the plain checks anywhere, the pinned-Lean local checks where Lean is installed, and native suites on a runtime.
Written against lema-lang at commit 5a94951, 17 Oct 2026.