my-lean

A monorepo containing my personal Lean projects.

Projects

The shared package keeps the toolchain, dependency lockfile, and build commands in one place.

All libraries share Batteries, pinned to v4.32.0 to match lean-toolchain, and use its linter. theory-of-computation/ and misc/ additionally depend on Mathlib (also v4.32.0, which pins the same Batteries revision) — for automata and formal languages, and for number theory respectively. After cloning or running lake update, fetch the prebuilt Mathlib artifacts with lake exe cache get — otherwise the first build compiles Mathlib from source.

To have this happen automatically in new worktrees, point git at the tracked hooks once per clone: git config core.hooksPath .githooks. The post-checkout hook there runs lake exe cache get whenever a fresh worktree is created.

distsys/veil-consensus/ is the exception to the shared package: it is a standalone Lake project on Lean v4.28.0 that depends on Veil, and it is not part of the root build. See distsys/README.md.

For quick throwaway experiments, create scratch.lean in the repo root — it's gitignored and checked live by the Lean editor extension (not part of any build).

Building

Build all libraries from the repo root:

lake build

To build one library only, name its Lake target, for example lake build TheoryOfComputation.

Linting

Run the Batteries linter over all libraries:

lake lint

CI uses leanprover/lean-action to run the same build and lint checks.