Related project -- Handwave

[lolipopshock]

@sepo-agent /answer

Can you take a look at this project https://github.com/quasisphere/handwave and compare how it connects with our lean workspace project?

[sepo-agent-app]

Short answer: Handwave looks complementary, not a replacement.

Handwave is a VS Code extension for annotated Lean projects: it indexes .lean files, reads %%handwave doc blocks, and renders .hw.md / .hw article files in an editor preview with declaration links, backlinks, dependency views, and Lean status badges (README, features). Our Lean workspace is a repo template for blueprint-as-source formalization, static previews, CI sync, and in-repo agent collaboration (README).

The main connection is the prose-to-Lean binding model:

• Handwave puts structured prose next to ordinary Lean declarations with %%handwave, then articles link/include declarations with lean:My.result (sample Lean, sample article).
• Our workspace puts blueprint items in content/blueprint/, either as markdown plan chapters with uses=, or literate Lean chapters where /-! ... -/ prose and declarations live together; lean=next binds an item to the next declaration (grammar, demo chapter).

They also overlap on status semantics. Handwave badges distinguish checked, stale, blocked, and sorryAx-dependent declarations, using .ilean / .olean artifacts and lake env lean --stdin for dependency probing (Handwave README, artifact extractor). Our workspace computes committed kernel truth through lake exe blueprint-data, recording used constants, axioms, and hasSorry into blueprint-data.json, then regenerates the canvas (BlueprintData.lean, status extraction).

Important difference: Handwave is editor-local and read-only preview oriented. Our workspace is repository/publication oriented: Lake roots are configured in lakefile.toml and blueprint.config.json, generated files are committed, CI refreshes data/canvas, and deployment does not need a Lean toolchain (lakefile, config, reference).

Practical integration options:

1. Treat Handwave as a VS Code companion for authors working inside a Lean workspace. Low risk, no template change required.
2. Add a converter/importer from .hw.md articles into content/blueprint/*.md, mapping @include{lean:X} to blueprint items with lean="X". This would need label generation and explicit uses= recovery.
3. Add optional support for reading %%handwave blocks as prose metadata when generating blueprint chapters. This is plausible, but it would be an extra authoring mode.
4. Borrow implementation ideas from Handwave’s .ilean / .olean artifact cache if we want faster local incremental status refresh. Our current CI-oriented extractor is simpler and deterministic, so I would not replace it wholesale.

Recommendation: position Handwave as an editor-layer inspiration/companion. If we want a concrete follow-up, the most useful first experiment is a small importer: samples/natural-numbers.hw.md + samples/Nat.lean -> native content/blueprint/ chapter with lean= bindings, then compare the generated blueprint canvas against Handwave’s preview model.

---

codex | gpt-5.5/xhigh | Macmini-runner-2