Reference
Commands, server methods, formats, rules and definitions, described exactly as the code at this commit implements them.
Reference pages describe; they do not teach. Look things up here when you need an exact flag, field, rule or theorem name. Where a feature is tested but its native suite has not been run, or is retired but still in the tree, the page says so.
- The lema command Every subcommand of the lema binary, with its flags, what it prints and how it exits.
- Server methods The request protocol of lema serve and every method it answers, with parameters and results.
- Runtime configuration The file that names the pinned Lean, the output directory and the shared lock, and the limits every native call runs under.
- Restricted Lean What the Lean source sent to elaborate and publish may contain, and how the server turns it into a draft of objects.
- Objects and identity The canonical object kinds a store holds, their exact fields, how each ID is computed, and how receipts record acceptance.
- Axiom policy and the fixed floor Which axioms an accepted object may depend on, how a store's policy is set, and how the footprint is audited at replay.
- Contract syntax The read-only text form in which the view method shows stored laws and definitions, with its constructs, precedences and faithfulness tests.
- Execution manifests The lema.exec/v1 record that names a program over accepted objects, its fields, entry kinds, IR profiles and the checks a build applies.
- Store records The records a store keeps beside its objects, such as aliases, bundles, revisions, policies and releases, with their fields and IDs.
- Program core The Core v2 definitions and theorems for programs that issue typed commands, with the companion modules built on them and their status.
- Standard library Each library module in lean/std, lean/json and lean/data, with its purpose, main theorems and whether it has been accepted through a store.
- Trusted base What Lema checks with the kernel, what it tests by running, what it assumes without proof, and what it does not claim.
- Requirements and environment variables What a machine needs to build lema and to make native calls, and every environment variable the tools and test suites read.
- Glossary The terms these docs use, each defined in a sentence or two, with the page that covers it.