feat: add progress tracking commands and auto-blueprinting - #11

Open

Deep0Thinking wants to merge 12 commits into

hanwenzhu:mainfrom

Deep0Thinking:main

Commits on Apr 8, 2026

feat: add blueprint progress stats
Deep0Thinking
committed
adb6a74
docs: add progress stats section to README
Deep0Thinking
committed
d76bdcb
feat: add per-module breakdown, multi-module support, and `local`/`nobreakdown` options
Deep0Thinking
committed
fbda12c
feat: add `#blueprint_status` command for per-node formalization status
Deep0Thinking
committed
fe9f7ac
feat: add `#blueprint_next` command to list incomplete nodes with dependency progress
Deep0Thinking
committed
75afdc6
feat: add `#blueprint_impact` command, improve formatting, and align naming
Deep0Thinking
committed
326f8f7
feat: add `blueprint.all` option to auto-blueprint declarations with docstrings
Deep0Thinking
committed
dc5b5e2
chore: rename `ImpactTest.lean` to `Commands.lean`
Deep0Thinking
committed
74f80ac
chore: adapt new files to module system and fix private visibility
Deep0Thinking
committed
69bdf56

Commits on May 13, 2026

feat: honor `blueprint.all` in the extractor and use docstrings for bare `@[blueprint]`

Deep0Thinking
and
claude
committed
b0e144b
fix: auto-nodes emit `\lean{}`, bogus `\mathlibok`, and no `\uses{}` edges

Deep0Thinking
and
claude
committed
4400504
docs: README — customizing the LaTeX environment under `blueprint.all`

Deep0Thinking
and
claude
committed
783e404