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 |
ai/ | Machine learning and neural networks |
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/, misc/, and ai/ additionally depend on
Mathlib (also v4.32.0, which
pins the same Batteries revision) — for automata and formal languages, for
number theory, and for analysis and linear algebra 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.