Add an opt-in native Lean 4 grammar - #664
Closed
odvcencio wants to merge 1 commit into
Closed
Conversation
- Add opt-in Lean 4 grammar authored with the Go DSL. The grammar targets Lean 4.32.2 and provides stable nodes for core declarations. Extension-specific syntax remains in line-scoped custom_command nodes because Lean modules extend the parser at runtime. - Add external scanner for nested block comments, documentation comments, and module documentation comments. - Add highlight captures and outline tags queries for editor integration. - Extend RegisterExtension to accept GrammarSource and TagsQuery fields. An empty GrammarSource defaults to GrammarSourceGrammargen. This lets external packages declare blob-based grammars and symbol extraction without calling Register directly. - Add corpus characterization test that validates 3,699 files from the official Lean 4.32.2 source without recovery nodes or early stops. - Keep the grammar opt-in to preserve the default 206-language graduation gates.
Owner
Author
|
Integrated into |
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
grammars/leanmodule.RegisterExtensionwith optional source and tags metadata.Scope
Lean modules can extend their parser at runtime. This grammar gives core declarations stable nodes. It preserves unknown extension syntax as line-scoped
custom_commandnodes.The grammar targets Lean 4.32.2 at commit
f3b06c705e6c85f5314019d5d3baab0fec5b580c.Validation
Graduation
This pull request keeps Lean opt-in. It does not change the default registry or its 206-language receipts. A later promotion can update the fleet gates to 207 languages.