my-lean

A monorepo containing my personal Lean projects.

Projects

Directory	Description
theory-of-computation/	Theory of computation exercises
functional-programming/	Functional programming exercises
distsys/	Distributed systems notes & exercises
misc/	Suff that doesn't fit above

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.