A collection of Lean 4 libraries for building applications with terminal UIs, graphics, networking, web frameworks, and data management.
lean-workspace/
├── graphics/ # Graphics & UI (11 projects)
├── math/ # Scientific & Math (2 projects)
├── web/ # Web Framework Stack (7 projects)
├── network/ # Networking & Protocols (4 projects)
├── audio/ # Audio (1 project)
├── data/ # Data & Storage (10 projects)
├── apps/ # Applications (12 projects)
├── util/ # CLI & Utilities (10 projects)
└── testing/ # Testing (1 project)
| Project | Description |
|---|---|
| afferent | 2D/3D graphics and UI framework with Metal GPU rendering (macOS); includes Afferent.Arbor/Afferent.Canopy |
| afferent-demos | Standalone demo runner for the Afferent graphics framework |
| terminus | Terminal UI library (ratatui-style) with widgets, layouts, and styling |
| trellis | Pure CSS layout computation (Flexbox and Grid) |
| tincture | Color library with RGBA/HSV support and color operations |
| chroma | Color picker application built on afferent (Afferent.Arbor widgets) |
| grove | Desktop file browser using afferent (Afferent.Arbor/Canopy) |
| assimptor | 3D model loading via Assimp FFI (FBX, OBJ, COLLADA) |
| worldmap | Tile-based map viewer with Web Mercator projection |
| vane | Hardware-accelerated terminal emulator using Metal (WIP) |
| raster | Image loading, saving, and manipulation via stb_image |
| Project | Description |
|---|---|
| linalg | Linear algebra library for game math (vectors, matrices, quaternions) |
| measures | Type-safe units of measure with compile-time dimension checking |
| Project | Description |
|---|---|
| loom | Rails-like web framework integrating Citadel, Scribe, and Ledger |
| citadel | HTTP/1.1 server with routing, middleware, and SSE support |
| herald | HTTP/1.1 message parser (requests, responses, chunked encoding) |
| scribe | Type-safe monadic HTML builder with HTMX integration |
| markup | Strict HTML parser producing Scribe Html values |
| chronicle | File-based logging library with text/JSON formats and Loom integration |
| stencil | Mustache/Handlebars-style template engine outputting Scribe Html |
| Project | Description |
|---|---|
| wisp | HTTP client library with libcurl FFI bindings |
| legate | Generic gRPC library with all streaming modes |
| protolean | Protocol Buffers implementation with compile-time proto_import |
| oracle | OpenRouter API client with streaming and tool calling |
| Project | Description |
|---|---|
| fugue | Functional sound synthesis library with macOS AudioToolbox FFI |
| Project | Description |
|---|---|
| ledger | Datomic-like fact-based database with time-travel queries |
| quarry | SQLite library with vendored amalgamation (no system dependencies) |
| chisel | Type-safe SQL DSL with compile-time validation |
| cellar | Generic disk cache library with LRU eviction |
| collimator | Profunctor optics library (lenses, prisms, traversals) |
| convergent | Operation-based CRDTs for distributed systems |
| reactive | Reflex-style functional reactive programming (FRP) |
| tabular | CSV/TSV parser with typed column extraction |
| entity | Archetypal Entity-Component-System (ECS) library |
| totem | TOML configuration parser with typed extraction |
| Project | Description |
|---|---|
| homebase-app | Personal dashboard with Kanban, auth, and multiple sections |
| todo-app | Demo todo list application built with Loom |
| enchiridion | Terminal novel writing assistant with AI integration |
| lighthouse | Terminal UI debugger/inspector for Ledger databases |
| blockfall | Terminal Tetris-like falling block puzzle game |
| twenty48 | Terminal 2048 sliding puzzle game |
| ask | Minimal CLI for talking to AI models on OpenRouter |
| cairn | Minecraft-style voxel game with Metal rendering |
| minefield | Terminal Minesweeper game with keyboard controls |
| solitaire | Terminal Klondike Solitaire card game |
| tracker | Local git-friendly issue tracker with CLI and TUI modes |
| timekeeper | Terminal time tracking app with categories and reports |
| Project | Description |
|---|---|
| parlance | CLI library with argument parsing, styled output, and progress indicators |
| staple | Essential utilities and macros (include_str% for compile-time file embedding) |
| chronos | Wall clock time library with nanosecond precision (POSIX FFI) |
| rune | Regular expression library with Thompson NFA simulation |
| sift | Parsec-style parser combinator library |
| conduit | Go-style typed channels for concurrency |
| docgen | Documentation generator for Lean 4 projects |
| tracer | Distributed tracing with W3C Trace Context support |
| crypt | Cryptographic primitives with libsodium FFI (hashing, encryption, HMAC) |
| timeout | Command timeout utility (shell script) |
| smalltalk | Smalltalk interpreter (WIP) |
| Project | Description |
|---|---|
| crucible | Lightweight test framework with declarative test macros |
Web Stack:
loom ───────────► citadel (HTTP server)
├──────────► scribe (HTML builder)
├──────────► ledger (database)
└──────────► herald (HTTP parser, via citadel)
citadel ────────► herald (HTTP parser)
markup ─────────► scribe (HTML types)
stencil ────────► scribe (HTML output)
homebase-app ───► loom (web framework)
todo-app ───────► loom (web framework)
Graphics Stack:
afferent ───────► collimator (profunctor optics)
├──────► wisp (HTTP client)
├──────► cellar (disk cache)
├──────► trellis (layout)
├──────► tincture (color)
├──────► Afferent.Arbor/Canopy (widgets)
└──────► assimptor (3D models)
afferent-demos ─► afferent (rendering + demos)
chroma ─────────► afferent (rendering + widgets)
worldmap ───────► afferent (rendering)
├──────► wisp (HTTP client)
└──────► cellar (disk cache)
vane ───────────► afferent (rendering)
Other:
legate ─────────► protolean (protobuf serialization)
oracle ─────────► wisp (HTTP client)
enchiridion ───► terminus (terminal UI)
└──► wisp (HTTP client)
lighthouse ────► terminus (terminal UI)
└───► ledger (database)
blockfall ─────► terminus (terminal UI)
twenty48 ──────► terminus (terminal UI)
minefield ─────► terminus (terminal UI)
solitaire ─────► terminus (terminal UI)
tracker ───────► terminus (terminal UI)
├──────► parlance (CLI library)
└──────► chronos (timestamps)
timekeeper ────► terminus (terminal UI)
└───► chronos (timestamps)
ask ───────────► parlance (CLI library)
└──────────► oracle (OpenRouter client)
docgen ────────► parlance (CLI library)
├───────► scribe (HTML generation)
└───────► staple (file embedding)
Each project is built independently from its directory:
cd <category>/<project>
lake build
lake test # if availableExamples:
cd graphics/terminus && lake build # Build terminus
cd web/loom && lake build # Build loom
cd apps/blockfall && lake build # Build blockfallSome projects require custom scripts (notably graphics/afferent, graphics/chroma, graphics/assimptor, graphics/raster, graphics/grove, data/quarry, audio/fugue, graphics/vane, and apps/cairn use ./build.sh for special build requirements). See individual project READMEs for specific build instructions.
The workspace includes a justfile for common operations. Run just to see all recipes:
# Git/submodule operations
just status # Show status of all submodules
just fetch # Fetch from all remotes
just pull # Pull latest in all submodules
just push # Push submodules with unpushed commits
# Building and testing
just build <category>/<project> # Build a specific project
just build-all # Build all projects
just test <category>/<project> # Test a specific project
just test-all # Test all projects
# Utilities
just versions # Show Lean versions across all projects
just lines # Count lines of Lean code
just deps # Show dependency graphHelper scripts in scripts/ for advanced operations:
./scripts/git-status.sh # Check which projects have changes
./scripts/git-add-commit-push.sh "msg" # Stage, commit, and push all
./scripts/count-lean-lines.sh # Count Lean code lines- Lean 4.26.x (check individual
lean-toolchainfiles) - Platform-specific dependencies vary by project (see individual READMEs)
All projects are MIT licensed. See individual LICENSE files.