Lentil

Lentil is a compile-time dependency-injection library for Lean 4. Definitions and structures register construction recipes with @[lentil]; composition commands check the resulting dependency graph during elaboration and generate ordinary Lean construction code.

Important

Lentil is pre-release software. The 0.1.0 module version is a development coordinate, not a compatibility promise, and public APIs may change before the first release.

import Lentil

open Lentil

structure Config where
  port : Nat

structure Server where
  config : Config

@[lentil] def config : IO Config := pure ⟨8080⟩
@[lentil] def server (config : Config) : Server := ⟨config⟩

@[lentil]
structure Service where
  server : Server
  label : String := "production"

make_context AppContext

def main : IO Unit := do
  let context ← AppContext.build
  IO.println s!"{context.service.label}: {context.service.server.config.port}"

Current scope

The implemented surface includes:

• definition recipes returning a value or IO action, with named explicit parameters treated as bean dependencies;
• zero-parameter structures whose non-defaulted fields are dependencies and whose defaulted fields retain their Lean defaults;
• priority-based provider selection, dependency-cycle detection, and missing or ambiguous provider diagnostics;
• closure-scoped construction with wire, whole-registry generated contexts, prototype construction through Bean.make, and typed context access through Has;
• persistent registration metadata across transitive imports, plus validate_beans and #bean_graph composition-root checks; and
• environment-backed configuration beans through @[lentil_config "PREFIX_"].

Recipes are currently restricted to closed, monomorphic Type 0 values and plain or IO results. Parameterized structures, universe-polymorphic recipes, request/session scopes, automatic cleanup, and runtime graph mutation are out of scope. Lentil generates and typechecks code, but it does not prove semantic properties of a recipe or of the runtime resources it constructs.

Prerequisites

• Bazel or Bazelisk using .bazelversion (currently Bazel 8.5);
• Nix, used by the repository's rules_lean toolchain; and
• for editor support, the Lean toolchain named in lean-toolchain.

Bazel is the authoritative build and test interface. The Lake project mirrors the source layout for editor tooling and direct developer builds.

Install the editor toolchain with Elan from the repository root:

elan toolchain install "$(cat lean-toolchain)"

Build from a checkout

bazel build //...
bazel test //...
lake build

Source-checkout consumer setup

Until registry releases are published, put a Lentil checkout next to the consuming repository and configure the consuming root module as follows:

bazel_dep(name = "lentil", version = "0.1.0")
local_path_override(module_name = "lentil", path = "../lentil")

# Overrides declared by dependencies are not inherited by a root module.
bazel_dep(name = "rules_lean", version = "0.1.0")
archive_override(
    module_name = "rules_lean",
    integrity = "sha256-R04+5hNuca2KRdLDQDnQ68hZYjpKcw6p6kz/aU/fmAc=",
    strip_prefix = "rules_lean-fbc2dd0626da1dee86348ff4841798ea8c8cbb34",
    urls = [
        "https://github.com/pb64-lean/rules_lean/archive/fbc2dd0626da1dee86348ff4841798ea8c8cbb34.tar.gz",
    ],
)

lean = use_extension(
    "@rules_lean//lean:extensions.bzl",
    "lean",
    dev_dependency = True,
)
lean.nix_toolchain(
    name = "lean4",
    attr = "lean4_upstream_std",
    nix_file = "@rules_lean//:nixpkgs.nix",
    nix_file_deps = ["@rules_lean//:nixpkgs.json"],
)
use_repo(lean, "lean4_toolchain")
register_toolchains(
    "@lean4_toolchain//:all",
    dev_dependency = True,
)

The consuming root owns this development-only toolchain block and can replace the Nix toolchain with another rules_lean toolchain. Marking it as a development dependency keeps that choice from leaking if this consumer is itself used as a dependency; it remains active for the root module's builds.

A minimal library target is:

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

lean_library(
    name = "app",
    srcs = ["App.lean"],
    deps = ["@lentil//:lentil"],
)

import Lentil

open Lentil

structure Message where
  text : String

@[lentil] def message : Message := ⟨"hello"⟩

def loadMessage : IO Message := wire Message

The checked-in downstream fixture exercises this consumer-owned dependency and toolchain boundary. For a Lake-only editor project using the same sibling checkout, add this to its lakefile.lean:

require «lentil» from "../lentil"

Recipes and components

Annotate a definition to register its result type. Named explicit parameters are dependencies, and instance-implicit parameters continue to be resolved by Lean's typeclass system:

@[lentil] def repository (config : Config) : Repository := ⟨config⟩
@[lentil] def client [HttpTransport] (config : Config) : IO Client :=
  Client.connect config

Annotating a structure gives it class-like constructor behavior: fields without defaults are injected, while ordinary Lean defaults are evaluated for defaulted fields.

@[lentil]
structure Service where
  repository : Repository
  displayName : String := "api"

Providers use Lean attribute priorities. The highest-priority provider for a type wins; validate_beans, wire, and make_context reject equal highest priorities as ambiguous.

@[lentil low] def fallbackConfig : Config := fallback
@[lentil] def normalConfig : Config := standard
@[lentil high] def productionConfig : Config := production
@[lentil 2000] def explicitPriorityConfig : Config := override

Construction

wire T builds only the registered dependency closure of T. Each selected type is constructed once within that plan, so diamond dependencies share the same value.

def start : IO Service := wire Service

Every registration also generates a Bean T instance. Calling Bean.make (α := T) uses ordinary recursive typeclass construction and has prototype semantics: separate calls, including separate branches in a diamond, may construct separate values.

wire, validate_beans, and make_context require each planned dependency to have registry metadata from @[lentil] or @[lentil_config]. A handwritten Bean instance participates in direct Bean.make typeclass construction, but not in generated singleton plans.

make_context Name validates the effective registry and emits:

• a Name structure containing every selected registered bean;
• Name.build : IO Name, which constructs and shares the values; and
• Has Name T instances for typed access with Lentil.get.

make_context AppContext

def run : IO Unit := do
  let context ← AppContext.build
  let service : Service := Lentil.get context
  IO.println service.label

Registrations are stored in a persistent Lean environment extension. A composition root therefore sees exactly the beans in its transitive import closure. A small imports-only module can serve as an explicit component-scan boundary.

Use validate_beans at a composition root to check its effective registry without generating a context. #bean_graph logs the registry in a Mermaid-style flowchart TD form for inspection.

Environment configuration

@[lentil_config] combines Lentil with the independent Config.Config environment decoder:

import Lentil

open Lentil EnvConfig

@[lentil_config "APP_"]
structure AppConfig where
  port : Nat := 8080
  publicUrl : String

#synth FromEnv AppConfig
#synth EnvPrefix AppConfig
#synth Bean AppConfig

The string argument is the exact prefix, including any desired separator. The attribute derives FromEnv, creates EnvPrefix, and registers a zero-argument IO AppConfig bean. Priorities use the same trailing syntax as ordinary beans, for example @[lentil_config "APP_" high] or @[lentil_config "APP_" 2000].

Config.Config does not depend on Lentil and remains usable by itself with deriving FromEnv, a separate EnvPrefix instance, and loadConfig. See the configuration reference for environment naming, built-in parsers, defaults, nesting, validation, and customization.

Development

Run both Bazel tests and the Lake build before sending a change.

• Configuration reference
• Changelog
• Contributing
• Code of Conduct
• Security

License

Licensed under the Apache License 2.0.