feat: add progress tracking commands and auto-blueprinting - #11
Open
Deep0Thinking wants to merge 12 commits into
Open
feat: add progress tracking commands and auto-blueprinting#11Deep0Thinking wants to merge 12 commits into
Deep0Thinking wants to merge 12 commits into
Conversation
Add `#blueprint_progress` command and `stats` CLI subcommand to display formalization progress stats.
…breakdown` options - `#blueprint_progress` now aggregates across all imports with per-module breakdown - Add `local` and `nobreakdown` options (`#blueprint_progress [local] [nobreakdown]`) - CLI `stats` accepts space-separated modules with `--local`/`-l` and `--nobreakdown`/`-n` flags - Fix percentage rounding to be consistent between aggregate and per-module
…endency progress
…naming - Add `#blueprint_impact` to show reverse dependencies and which nodes would be unblocked by formalizing a given node - Rename `#blueprint_next` to `#blueprint_incomplete` - Rename CLI `stats` to `progress` to match `#blueprint_progress` - Show `n/m (pct%)` format with aligned columns across all commands - Show dep fraction and status in Blocking and Would-unblock sections - Omit module column in interactive output (names are clickable) - Unify node structures into shared `NodeEntry` with `DepFracWidths`
…docstrings - `set_option blueprint.all true` includes all docstring'd declarations in the blueprint without requiring explicit `@[blueprint]` tags - Statement text comes from docstring, latexEnv from declaration kind, dependencies and status are auto-inferred as usual - Explicit `@[blueprint ...]` overrides auto-mode for specific declarations - Declarations without docstrings are excluded (docstring is the opt-in signal) - Scope is current file only; imported modules are not auto-blueprinted - Add `findBlueprintNode?` and `getLocalBlueprintNodes` wrappers to transparently handle auto-nodes alongside explicitly tagged nodes - Add `MonadOptions` constraint to `collectUsed` and output functions
…are `@[blueprint]` `set_option blueprint.all true` previously only affected interactive commands; `lake build :blueprint` (which runs the extractor in a separate process) ignored it, so auto-blueprinted declarations never reached the generated blueprint. - `getBlueprintContents` now also materializes auto-nodes for the module being extracted when `blueprint.all` is set in the passed options (set it via the lakefile's `leanOptions` so the extractor receives it). - A bare `@[blueprint]` (no `statement := ...`) now uses the declaration's docstring as its statement, matching auto-mode instead of rendering empty. - README: document the lakefile `leanOptions` route and the docstring fallback. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…edges
Auto-nodes (from `blueprint.all`) are materialized at extraction time and never
register a `latexLabel → Lean name` mapping the way the `@[blueprint]` attribute
does. So in `NodeWithPos.toLatex`, `getLeanNamesOfLatexLabel` returned `[]` and
`allNodes` was empty, causing: empty `\lean{}`, a vacuously-true `\mathlibok`,
and no `\uses{}` edges (the dependency graph had no edges).
- `NodeWithPos.toLatex`: fall back to the node's own name when no label mapping
is registered.
- `mkAutoNode`: never auto-blueprint declarations from library modules
(`Init`/`Lean`/`Std`/`Batteries`/`Mathlib`), so inferred `\uses{}` edges point
only at project nodes that actually exist in the blueprint, not at e.g. `Eq`.
- Factor the library-module check into `isLibraryDecl`; reuse it for `isMathlibOk`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add a subsection explaining why auto-mode renders `lemma`/`proposition`/etc.
as `\begin{theorem}` (Lean discards the surface keyword across the Mathlib
macro expansion to `theorem`), with two recipes for controlling the env:
per-declaration `@[blueprint (latexEnv := ...)]` and a project-side
`macro_rules` block (in a drop-in `MyProject/Blueprint.lean`) that attaches
the attribute automatically. The macro form captures the optional
`docComment` separately so the rewritten attribute lands in the resulting
`theorem`'s own modifiers, sidestepping the `declModifiers`-slot conflict
that breaks the more obvious shape.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add interactive and CLI commands for tracking formalization progress, plus an auto-blueprinting mode.
Demo
LeanArchitect_new_commands_PR_demo.mov
Progress tracking
4 new commands, each with a corresponding CLI subcommand:
#blueprint_progress#blueprint_incomplete#blueprint_status <node_name>#blueprint_impact <node_name>All support a
localmodifier to restrict scope to the current file/given modules.Auto-blueprinting
set_option blueprint.all trueincludes all declarations with docstrings in the blueprint without requiring@[blueprint]tags. The docstring becomes the statement text, the LaTeX environment is inferred from the declaration kind, and explicit@[blueprint ...]takes precedence. Scope is current file only.Co-authored-by: Claude (Opus 4.6) claude@anthropic.com