[Documentation] Simplify Compiler/Proofs/README.md (324→109 lines)#63
Merged
[Documentation] Simplify Compiler/Proofs/README.md (324→109 lines)#63
Conversation
Remove duplicate build commands (Quick Start and Testing sections were identical), fix wrong "Expected Warnings: None" claim (sum properties produce sorry warnings), and consolidate verbose sections into compact format. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Th0rgal
pushed a commit
that referenced
this pull request
Feb 14, 2026
Closes #86 ### Summary Added comprehensive "Code Comment Conventions" section to CONTRIBUTING.md to prevent future documentation drift and establish clear standards. ### What's Included **Proof Status Conventions**: - Clear rules for when to use `sorry` vs no marker - Prohibition on TODO/STUB in proven theorems - Examples of good vs bad patterns **Module Documentation**: - Standard header format with Status/Dependencies - Clear status definitions (Complete/Partial/Draft) - Example template **Future Work Comments**: - Use `FUTURE:` instead of `TODO:` - Always link to tracking issue - Avoid FIXME/HACK **Implementation Notes**: - Use `NOTE:` for non-obvious design choices - Explain why, not just what - Reference related files **Axiom Documentation**: - Inline comment requirements - Link to AXIOMS.md - Consistent format **Property Test Tags**: - Must match Lean theorem names exactly - Standard tag format **What NOT to Include**: - Stale TODOs in completed code - Difficulty estimates after completion - Verbose explanations of obvious code - Inaccurate status claims ### Context Issue #86 identified stale TODO comments and inconsistent status claims. Recent refactoring commits (see #61, #62, #63) cleaned up the actual issues: - Removed 151 lines of stale planning comments - Deleted dead reentrancy wrappers - Fixed stale YulGeneration README - Removed 162 lines of stale/duplicate content This PR completes #86 by documenting conventions to prevent recurrence. ### Impact **Before**: - ❌ No documented comment conventions - ❌ Inconsistent status markers - ❌ TODOs in completed code - ❌ No guidance for contributors **After**: - ✅ Clear comment conventions documented - ✅ Standard status definitions - ✅ Examples of good/bad patterns - ✅ Prevents future documentation drift **For Contributors**: - Clear guidelines on code comments - Prevents misleading documentation - Consistent style across codebase - Easier code review ### Files Changed - `CONTRIBUTING.md`: Added 130-line "Code Comment Conventions" section ### Related Work Recent cleanup commits that addressed the actual issues: - #61: Delete dead reentrancy wrappers, clean stale proof comments - #62: Remove 151 lines of stale planning comments from proofs - #63: Simplify Compiler/Proofs/README.md from 324 to 109 lines Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Th0rgal
added a commit
that referenced
this pull request
Feb 14, 2026
Closes #86 ### Summary Added comprehensive "Code Comment Conventions" section to CONTRIBUTING.md to prevent future documentation drift and establish clear standards. ### What's Included **Proof Status Conventions**: - Clear rules for when to use `sorry` vs no marker - Prohibition on TODO/STUB in proven theorems - Examples of good vs bad patterns **Module Documentation**: - Standard header format with Status/Dependencies - Clear status definitions (Complete/Partial/Draft) - Example template **Future Work Comments**: - Use `FUTURE:` instead of `TODO:` - Always link to tracking issue - Avoid FIXME/HACK **Implementation Notes**: - Use `NOTE:` for non-obvious design choices - Explain why, not just what - Reference related files **Axiom Documentation**: - Inline comment requirements - Link to AXIOMS.md - Consistent format **Property Test Tags**: - Must match Lean theorem names exactly - Standard tag format **What NOT to Include**: - Stale TODOs in completed code - Difficulty estimates after completion - Verbose explanations of obvious code - Inaccurate status claims ### Context Issue #86 identified stale TODO comments and inconsistent status claims. Recent refactoring commits (see #61, #62, #63) cleaned up the actual issues: - Removed 151 lines of stale planning comments - Deleted dead reentrancy wrappers - Fixed stale YulGeneration README - Removed 162 lines of stale/duplicate content This PR completes #86 by documenting conventions to prevent recurrence. ### Impact **Before**: - ❌ No documented comment conventions - ❌ Inconsistent status markers - ❌ TODOs in completed code - ❌ No guidance for contributors **After**: - ✅ Clear comment conventions documented - ✅ Standard status definitions - ✅ Examples of good/bad patterns - ✅ Prevents future documentation drift **For Contributors**: - Clear guidelines on code comments - Prevents misleading documentation - Consistent style across codebase - Easier code review ### Files Changed - `CONTRIBUTING.md`: Added 130-line "Code Comment Conventions" section ### Related Work Recent cleanup commits that addressed the actual issues: - #61: Delete dead reentrancy wrappers, clean stale proof comments - #62: Remove 151 lines of stale planning comments from proofs - #63: Simplify Compiler/Proofs/README.md from 324 to 109 lines Co-authored-by: Claude Sonnet 4.5 <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.
Summary
lake buildcommands)SumProofs.lean,Sum.lean) produce expectedsorrywarningsTest plan
lake buildpasses (77/77 modules, only expectedsorrywarnings)🤖 Generated with Claude Code
Note
Low Risk
Documentation-only changes; no impact on compiler or proof logic, aside from clarifying known build warnings.
Overview
Simplifies
Compiler/Proofs/README.mdby condensing the compiler-proof overview, build instructions, infrastructure notes, proof patterns, and tactics into a shorter, more skimmable document.Removes duplicated/overly detailed sections (extended lemma listings, testing/contributing guidance), updates Layer 1/3 descriptions, and documents expected
sorrywarnings for the WIP sum proofs (DumbContracts.Specs.Ledger.SumProofs,DumbContracts.Specs.Common.Sum).Written by Cursor Bugbot for commit c647b5e. This will update automatically on new commits. Configure here.