Docs cleanup: drop stale spec, compress conventions and playbook (901 → 526 lines)#27
Merged
Conversation
901 → 526 lines (42% reduction) across docs/. Removes content that either duplicates CLAUDE.md, contradicts the current code, or has no behavioral payload. Removed entirely: - docs/RIEMANNIAN_FRAMEWORK_SPEC.md — orphan, never referenced; class definitions exist but adoption is incomplete (8 [RiemannianManifold] vs 17 [HasMetric] uses); notation table contradicts current code (claims `Δ_g f` but actual is `Δ_g[I] f`); anti-pattern §5 actively violated by current code. The class docstrings in Riemannian/Manifold/SmoothManifold.lean carry the design intent. CONVENTIONS.md (135 → 59): - Drop "v1 — Stage I" version metadata - Drop "Layer 1: Autonomy policy" section (now in CLAUDE.md as the Mathlib-wrapping policy) - Drop "Future sections" aspirational list - Keep: curvature sign, length functional, geodesic, mm-space NAMING_CONVENTION.md (177 → 91): - Keep: object suffixes, theorem suffixes, naming case, local notation, module docstring template, private/protected/public - Drop §6 (per-decl docstring) — duplicates Math/Eng/Mixed in CLAUDE.md - Drop §7 (engineering hiding) — duplicates anchor purity in CLAUDE.md - Drop §8 (UXTest sections) — was entirely "this is removed" history - Drop §10 (refactor process) — duplicates REFACTOR_PLAYBOOK - Drop §5 "Removed" blacklist subsection REFACTOR_PLAYBOOK.md (344 → 261): - Drop "Pre-flight checklist" — duplicates CLAUDE.md atomic-commit - Drop "Lake script vs bash" section — niche meta-tool guidance with no daily payload - Drop pitfall #7 (.gitkeep) — one-shot trivia - Drop "Adding to this playbook" meta epilogue - Keep: decision tree, the 8 substantive pitfalls, consolidation procedure SORRY_CATALOG.md untouched — data drift (catalog says 32, CI says 42) is a separate maintenance concern.
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.
Summary
Audited
docs/for redundancy and drift. Cut 42% (901 → 526 lines) across 4 files, removing content that either duplicates CLAUDE.md, contradicts the current code, or has no behavioral payload.Removed entirely
docs/RIEMANNIAN_FRAMEWORK_SPEC.md— orphan documentation. Verification (this PR):*.leanor*.md).class SmoothManifold/class RiemannianManifolddo exist inRiemannian/Manifold/SmoothManifold.lean, but adoption is incomplete: 8 uses of[RiemannianManifold M]vs 17 of[HasMetric I M].Δ_g f,grad_g f; actual code usesΔ_g[I] f,grad_g[I] f.[I]-bracket notation is legacy") is actively violated by current code.The design intent for
SmoothManifold/RiemannianManifoldis preserved in their own file's docstring.Compressed
CONVENTIONS.md(135 → 59) — kept the four substantive convention pinnings (curvature sign, length functional, geodesic, mm-space); dropped version metadata, the Mathlib-autonomy section (now in CLAUDE.md), and the aspirational "Future sections" list.NAMING_CONVENTION.md(177 → 91) — kept object/theorem suffixes, naming case, local notation, docstring template, private/protected/public; dropped §6 (per-decl docstring, duplicates Math/Eng/Mixed), §7 (engineering hiding, duplicates anchor purity), §8 (entirely "this is removed" history), §10 (refactor process, duplicates the playbook), and the §5 "Removed" blacklist.REFACTOR_PLAYBOOK.md(344 → 261) — kept decision tree, the 8 substantive pitfalls, consolidation procedure; dropped pre-flight checklist (duplicates CLAUDE.md atomic-commit), "Lake script vs bash" section (niche meta-tool guidance), the.gitkeeppitfall (one-shot trivia), and the meta epilogue.Not touched
SORRY_CATALOG.md— has its own data drift (catalog says 32, CI says 42) that's a separate maintenance concern.Test plan
RIEMANNIAN_FRAMEWORK_SPEC.md.SmoothManifoldandRiemannianManifoldadoption counts.Δ_g[I]/grad_g[I]/scal_g[I].