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_"];
• optional managed resource composition with rollback, phased cleanup, retained tasks, joined close, and separate readiness/liveness state.

Recipes are currently restricted to closed, monomorphic Type 0 values and plain or IO results. Parameterized structures, universe-polymorphic recipes, request/session scopes 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

Managed applications

Ordinary wire, Bean.make, and make_context remain construction-only. Use @[lentil_managed] on a definition returning IO (Resource T) to transfer cleanup obligations to a generated application owner:

@[lentil_managed] def database (config : Config) : IO (Resource Database) := do
  let db ← Database.connect config
  return { value := db, hooks := { release := db.close } }

@[lentil_managed] def listener (db : Database) : IO (Resource Listener) := do
  let listener ← Listener.start db
  return { value := listener, hooks := {
    quiesce := listener.stopAdmission
    drain := listener.join
    release := listener.release } }

make_managed_context AppContext

def run : IO Unit := do
  let app ← AppContext.build
  app.use fun context => do
    app.scope.markReady
    context.listener.waitForShutdown

The example resource types/methods are application-defined. Generated fields and Has access expose the underlying T, not Resource T. Plain recipes may depend on managed ones in this plan. Managed recipes deliberately have no Bean instance, and unmanaged plans reject a managed dependency closure.

Construction is dependency-first and singleton-sharing. Failed construction rolls back all resources already registered, including when a subsequent plain recipe fails. Each resource-producing action must clean any partial acquisition if it throws before returning Resource. Cleanup runs all quiesce hooks, then all drain hooks, then all release hooks, in reverse construction order within every phase. Dependencies stay available through dependent drains. Every quiesce/drain hook is attempted even after failures. If any drain fails, all releases are withheld and the scope retains the hooks: a database must not be closed underneath a still-running handler. CloseReport.releasesDeferred makes this explicit. Scope.resumeClose retries drains only (joining must be repeatable), then releases once after every drain succeeds. Release failures do not skip other release hooks and are never retried automatically because an underlying handle may already have been consumed. CloseReport names each resource, phase, and error. Application.use preserves body/cleanup failures.

Generated AppContext.tryBuild and the runtime tryBuildManaged return Except BuildFailure (Application T). A failure retains its primary error, cleanup report, and scope for explicit recovery if rollback cannot drain. Use this checked API for recoverable startup. The throwing .build convenience is intended for process-fatal startup; its exception cannot return ownership.

Scope.close is idempotent and joined: concurrent callers wait for one cleanup owner and receive the identical report, including errors. A close waits for an in-flight acquisition; acquisitions after closing starts fail without executing. Acquisition callbacks run under a scope mutex and must not re-enter their scope. Cleanup callbacks run outside the mutex but must not recursively close it. Hooks must terminate; this library intentionally cannot force a blocked resource to finish or claim it has drained after abandoning its task.

Scope.spawn name action stop retains a normal Lean IO task, invokes the cooperative stop action during quiesce, and joins/reports it during drain. stop must actually unblock the task: cancelling a task does not interrupt arbitrary blocking IO. No new scheduler, timeout runtime, or transport is added.

Scope.health starts live but not ready. Explicit markReady enables readiness; close withdraws readiness before invoking hooks and liveness remains true during cleanup. A deferred-drain failure makes liveness false and records drainFailed; the hooks remain retained for recovery. Consumers map this to their health protocol.

The runtime can be imported alone as Lentil.Managed (@lentil//:managed), without the DI elaborator or transports. Optional Lentil.Signals (@lentil//:signals) owns libuv SIGINT/SIGTERM waiters through a resource and offers nonblocking poll; it spawns no blocked continuation tasks. POSIX signal delivery is tested on Linux; no Windows SIGTERM guarantee is made.

Validation includes acquisition rollback, exact phased ordering, cleanup/body failure preservation, concurrent acquisition/close and repeated joined close, task failure/join tests, downstream generated contexts, and real process SIGINT/SIGTERM delivery. Run lake build managed_test signal_fixture in addition to the ordinary Lake developer checks.

Lentil.Cleanup defines the command program interpreted by managed scopes. The interpreter constructs an erased execution certificate from hook outcomes. Kernel-checked theorems establish the drain barrier before every release invocation, deferred releases after drain errors, reverse registration order, and omission of quiesce on resumed attempts. The barrier covers execution prefixes, including a pending hook that never finishes. These contracts concern hook invocation and return order; each hook owns the correctness of its IO and its resource's drainage. //lean/Lentil:cleanup_assurance checks the principal theorem statements and their axiom dependencies.

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.