rules_lean

Bazel build rules and Bzlmod toolchain configuration for Lean 4.

rules_lean compiles Lean modules, links native executables, runs Lean programs as Bazel tests, and makes locked or prebuilt Lake packages available to Bazel targets.

Setup

Add the module and register a Lean toolchain in MODULE.bazel:

bazel_dep(name = "rules_lean", version = "0.1.0")

lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
lean.local_toolchain(name = "lean4", expected_version = "4.31.0")
use_repo(lean, "lean4_toolchain")

register_toolchains("@lean4_toolchain//:all")

local_toolchain requires an absolute lean_home when provided. Otherwise it resolves lean from PATH, asks that executable for its installation prefix, and validates the version and complete Lean/Lake/header/runtime layout. When an expected_version differs from the PATH installation, it may use the compiler selected by elan which lean; it never reconstructs an Elan path from a version string.

The toolchain tag downloads supported official releases with checked-in SHA-256 digests and exact archive prefixes. A custom archive is accepted only when url, sha256, and strip_prefix are all provided. Caveat: of the digests pinned in lean/repositories.bzl (_LEAN4_RELEASES), CI exercises only v4.14.0 on linux-x86_64; the remaining version/platform entries fail closed on any digest mismatch, but a green CI run does not validate them end to end. The extension also supports Nix-provided toolchains through nix_toolchain. Their configuration is defined in lean/extensions.bzl.

A nix_toolchain keeps its realized output rooted through .lean-toolchain-gc-root in Bazel's generated repository. Removing that repository releases the root; ordinary Nix garbage collection cannot leave a still-cached Bazel toolchain pointing at a missing store path.

A C/C++ toolchain must be available because Lean sources are compiled to native objects and linked through Bazel's C++ toolchain.

Build rules

Load the rules from @rules_lean//lean:defs.bzl.

Rule	Purpose
lean_library	Compiles Lean modules and produces compiled Lean outputs, a static archive, and CcInfo.
lean_binary	Compiles and links a Lean program as a native executable.
lean_test	Compiles and links a Lean program and runs it with bazel test; its exit code is the test result.
lean_prebuilt_lake_library	Exposes an existing Lake cache as a Lean dependency, with optional lazy native linking.
lean_lsp_server	Runs the selected toolchain's Lean language server with the compiled, indexed, and source outputs of its dependency closure.
lean_assurance_test	Audits compiled Lean libraries for proof holes, axioms, and trust-boundary surface, with policy-driven failure.

For example:

load("@rules_lean//lean:defs.bzl", "lean_library", "lean_lsp_server", "lean_test")

lean_library(
    name = "hello",
    srcs = ["Hello.lean"],
)

lean_test(
    name = "hello_test",
    srcs = ["HelloTest.lean"],
    deps = [":hello"],
)

lean_lsp_server(
    name = "lean_lsp",
    deps = [":hello"],
)

Dependencies may provide Lean compilation information, C/C++ linking information, or both. lean_library can also generate a C header with hdrs_out and c_declarations for functions exported by Lean code.

Language server

lean_lsp_server is a no-argument executable entry point for editors and remote-development hosts:

bazel run //:lean_lsp

It executes lean --server from the caller's workspace directory with stdin, stdout, and stderr unchanged. The executable and standard-library paths come from Bazel's registered, platform-selected Lean toolchain; it never discovers a compiler through PATH or reconstructs an Elan directory. LEAN_PATH and LEAN_SRC_PATH are deterministic and include the transitive .olean, .ilean, normalized source, and Lake import outputs of deps. Bazel stages these files into the same unified module overlay used by Lean compilation, including only nonempty module sidecars (.ir, .olean.private, and .olean.server) because ordinary Lean rules declare empty placeholders for modules that do not produce them. The launcher therefore works from Bazel's runfiles tree as well as from workspace output symlinks without exposing invalid sidecars or separating a module from its transitive imports. Toolchain standard-library sources are used when the distribution supplies src/lean; source-stripped toolchains continue to work with the project source roots alone. Analysis fails when two source-built roots claim the same logical module, because one language-server process cannot serve two conflicting module families safely.

The launcher also disables Lean's implicit lake setup-file discovery. This prevents a colocated lockfile or Lake manifest from replacing the Bazel-built closure (or building into the source tree) when a buffer opens. Use lake serve directly for a Lake-owned project; lean_lsp_server is the Bazel-owned entry point.

Generated Lean sources

Action-owning rules that generate .lean files should return the public LeanGeneratedSourceInfo provider and expose the same direct source depset as the lean_srcs output group:

load("@rules_lean//lean:defs.bzl", "LeanGeneratedSourceInfo")

return [
    LeanGeneratedSourceInfo(lean_srcs = generated),
    OutputGroupInfo(lean_srcs = generated),
]

Because providers exist only after analysis, use cquery to discover and build every such generator in the current workspace:

set -o pipefail
bazel cquery 'kind(rule, //...)' \
  --output=starlark \
  --starlark:expr='str(target.label) if [key for key in providers(target) if key.endswith("//lean:providers.bzl%LeanGeneratedSourceInfo")] else ""' |
  sed '/^$/d' |
  sort -u |
  xargs -r bazel build --output_groups=lean_srcs

The provider is intentionally direct and belongs on the source-generating target, not on a compiled lean_library wrapper. The provider-key suffix is stable across Bzlmod canonical repository names; sort -u removes duplicate labels reached in multiple configurations.

Proof assurance

lean_assurance_test audits the compiled Environment of its deps while the generated test binary is compiled, so policy violations fail the build of the test target. A passing run prints a human-readable summary plus a JSON block (visible with --test_output=all).

load("@rules_lean//lean:defs.bzl", "lean_assurance_test")

lean_assurance_test(
    name = "mylib_assurance",
    deps = [":mylib"],
    policy_mode = "exact",
    principal_theorems = ["MyLib.main_theorem"],
    principal_theorem_types = {
        "MyLib.main_theorem": "∀ x : Nat, MyLib.normalize x = x",
    },
    allowed_axioms = ["propext", "Classical.choice", "Quot.sound"],
    module_prefixes = ["MyLib"],
    expected_unsafe_constants = [],
    expected_partial_definitions = [],
    expected_opaque_constants = [],
    expected_implemented_by = {},
    expected_extern_declarations = {},
    expected_native_targets = [],
)

policy_mode must always be written explicitly; omitting it fails at load time. Exact mode is the supported policy. Every field is explicit: theorem names are definitionally checked against their declared types, and unsafe, partial, non-proof opaque, @[implemented_by], @[extern], and reachable native Bazel targets must match exactly. Both additions and removals fail. An extern descriptor has the canonical form backend:kind:value (for example, c:standard:my_symbol); multiple entries are joined by |. Private names are normalized to stable user-facing, module-qualified names; a normalization collision fails when the collided name is one the report states something about (an inventory entry or a violation). Collisions among unreported compiler-generated helpers — e.g. the hygienic match_on_same_ctor pair that deriving BEq, DecidableEq emit — are tolerated.

Exact mode partitions the imported world at module granularity: every module in the transitive import closure of the audited environment must be covered by module_prefixes (audited by this target), unaudited_module_prefixes (explicitly declared out of scope), or the built-in toolchain allowlist (Init, Std, Lean, Lake — roots shipped inside the pinned Lean toolchain archive — plus RulesLean.Assurance, the audit framework itself). A module outside that partition fails the build with the offending module names; the fix is to extend module_prefixes, or to declare the modules in unaudited_module_prefixes when another audit or an explicit trust decision owns them. The rule records but cannot verify that another assurance target covers an unaudited prefix. The two prefix lists must not overlap (that would make a module's scope ambiguous), and only modules matching module_prefixes contribute to the inventories above.

Every audit also defines <name>_manifest, which writes <name>.assurance.txt and <name>.assurance.json after a passing audit.

The legacy mode is a deprecated, explicitly written opt-out: it is never the default, and every target that declares policy_mode = "legacy" prints a load-time deprecation warning in the build log, even on green runs. Its checks, scoped to modules matching module_prefixes (default: the direct deps' modules), are:

• Each principal theorem exists, is a theorem, and its axiom dependency closure (Lean.collectAxioms) stays within allowed_axioms (default: propext, Classical.choice, Quot.sound; sorryAx is never allowed).
• Constants whose dependency closure reaches sorryAx fail, as do axioms declared outside the allowed set and dependencies on disallowed axioms.
• @[extern] constants fail unless their module is covered by allowed_extern_modules; unsafe constants fail only with fail_on_unsafe = True; opaque constants and partial definitions are reported. As in exact mode, the reported opaque inventory covers only non-proof opaques: Prop-typed opaque constants are omitted.

See //lean/assurance/testdata for a green demo and automated negative fixtures that pass only while their expected policy violations are detected.

Portable static runtime

Shared runtime linking is the default: executables link -lleanshared, carry the toolchain runtime path, and include libleanshared in runfiles.

Portable static mode targets GNU/Linux. For a relocatable production executable, select it for the whole build:

bazel build --features=lean_static_runtime //path/to:lean_binary

The selected Lean toolchain must supply lib/lean/libleanportable.a and pass it as libleanportable to lean_toolchain. Generated archive, local, and Nix toolchain repositories expose that attribute automatically when the archive is present. Static mode enables linker --as-needed, then passes the same archive followed by the baseline system -lm to native link actions. The as-needed state prevents a C++ toolchain's later fallback -lstdc++ from restoring a shared runtime dependency after the archive resolved it. Static mode also removes the -lleanshared option, Lean runtime RUNPATH, and shared runtime runfiles from source-built libraries, binaries, tests, and Lake-built dependency CcInfo. In either mode the toolchain owns one canonical runtime LinkerInput; converging Lean/Lake/C++ dependency branches therefore emit the runtime archive or shared-library flags exactly once, after all Lean archives. Use the command-line feature (or an equivalent package-wide feature) so every configured target in the transitive closure selects the same runtime mode.

Lake dependencies

The lean.deps extension tag consumes a committed lake-manifest.json, fetches each git package at its locked revision, builds the manifest's package closure with Lake, and creates an @<repository>//<package> target for every package.

Using the extension from the setup above:

lean.deps(
    name = "lean_deps",
    manifest = "//:lake-manifest.json",
    lakefile = "//:lakefile.toml",
    lean_toolchain = "//:lean-toolchain",
    libraries = {"batteries": "Batteries"},
)
use_repo(lean, "lean_deps")

A first-party target can then depend on a locked package:

load("@rules_lean//lean:defs.bzl", "lean_library")

lean_library(
    name = "uses_batteries",
    srcs = ["UsesBatteries.lean"],
    deps = ["@lean_deps//batteries"],
)

Only git packages in the Lake manifest are supported. A TOML package with exactly one lean_lib is discovered automatically. Packages using lakefile.lean, or TOML packages with zero or multiple libraries, require an explicit libraries entry. The selected static archive is captured by name; missing or ambiguous outputs fail instead of silently selecting an arbitrary archive or generating an empty one. Manifest subDir paths are honored.

After changing the lakefile, run lake update and commit the refreshed manifest. When lean_toolchain is supplied, its version is checked against the registered Bazel toolchain before the Lake action runs.

Prebuilt Lake libraries

lean_prebuilt_lake_library is the generic bridge from an existing Lake cache to Bazel-native Lean targets:

load("@rules_lean//lean:defs.bzl", "lean_prebuilt_lake_library")

lean_prebuilt_lake_library(
    name = "prebuilt",
    srcs = glob([".lake/build/lib/lean/**"]),
    import_roots = [".lake/build/lib/lean/Package.olean"],
    native_srcs = glob([".lake/build/ir/**/*.c"]),
    expected_lean_version = "4.33.1",
)

Every import_roots file is a marker: its parent directory becomes one LEAN_PATH root, and cache files under that parent are staged with their relative paths intact. At least one marker is required. The registered Lean toolchain must match expected_lean_version (with an optional leading v ignored). Generated Lean C selected by native_srcs is compiled and archived only when a consumer requests the native CcInfo closure or the native output group; import-only default builds do not realize those outputs. Optional sources and the original cache inputs are available through the prebuilt_sources and prebuilt_cache output groups, respectively, and are not added to dependent executables' runfiles.

Mathlib cache

The lean.mathlib extension tag materializes an exactly locked Mathlib cache:

lean.mathlib(
    name = "mathlib",
    manifest = "//:lake-manifest.json",
    lean_toolchain = "//:lean-toolchain",
    module_roots = ["Mathlib.Data.Nat.Factorial.Basic"],
    allow_source_fallback = False,
)
use_repo(lean, "mathlib")

The committed root manifest must pin Mathlib to a full 40-character Git commit and contain every package in that checkout's own manifest. The manifest schema and each inherited package's type, url, rev, subDir, manifestFile, and configFile must match upstream exactly; dependency overrides fail.

The committed root lean-toolchain must match Mathlib's file byte-for-byte and contain one exact <origin>:v<version> pin. Both the selected Lean and Lake executables are checked against that version. Set toolchain to a registered extension toolchain name when more than one is declared; it is inferred only when exactly one exists. This selects the executables used during repository materialization. Configured targets still use normal Bazel toolchain resolution and fail the prebuilt version check if a different version is active, so only one Lean version should be registered for a given target configuration.

module_roots contains dotted Lean module names. The official cache command is asked for those roots and their transitive import closure, and each requested root must materialize a complete .olean, .ilean, IR/module-sidecar, and generated-C family. The cache client is first bootstrapped from the pinned checkout; all outputs from that helper build are discarded before the copied client materializes the official closure, so helper modules are never exposed as Mathlib dependencies. Cache command failures and incomplete transitive module families fail closed by default. Setting allow_source_fallback = True explicitly permits the same pinned, root-scoped library closure to be built from source, which can be substantially more expensive.

Examples

Each example is a standalone Bzlmod workspace:

• examples/download_toolchain verifies the SHA-pinned official archive toolchain end to end.
• examples/basic_lean builds a Lean library and runs Lean test programs.
• examples/lake_deps consumes a direct Lake package.
• examples/lake_transitive consumes a Lake package with a transitive dependency.
• examples/mathlib_deps consumes an exactly pinned subset of Mathlib through its official prebuilt cache and exercises native linking.