New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add a lexer for Lean 4 #2618
Add a lexer for Lean 4 #2618
Conversation
e0e4be3
to
a2266d1
Compare
…f53542814c79469711ceff19fbf/doc/latex/lean4.py This is based off an old version of the Lean 3 lexer.
There is no need for `re.UNICODE` any more, or `u` prefixes.
The version and url information no longer lives in the docstring.
58b75ee
to
843b426
Compare
This allows a lean4 version of the lean3 test to be committed
* Use `Whitespace` not `Text` for Whitespace * Use a single token for an entire multiline comment, not one per character * Fix brace-matching for `@[attr]` syntax * Add docstring highlighting
843b426
to
83209aa
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice! This looks pretty good. I'm sure I've missed a thing or two, but I tried to double check the keyword list and give a cursory look over the token list which pretty much looks good!
Maybe also add a line to the |
This also corrects the integer parser to not include field projections
7b89197
to
57f88c3
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice. This LGTM at this point I think (with or without the operator tweaking)!
(r'\d+', Number.Integer), | ||
(r'"', String.Double, 'string'), | ||
(r'[~?][a-z][\w\']*:', Name.Variable), | ||
(r'\S', Name.Builtin.Pseudo), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What is this rule for?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Arbitrary notation defined by the user; without it, all such notation would be marked as invalid
This looks generally good, only a couple minor questions above. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good. Thank you!
Thanks! I've made a small follow-up in #2626; it would be great if they could both land in the coming release. |
Sure, this will all be in 2.18. |
An improved `lean4` lexer is now part of pygments. This depends on pygments/pygments#2618 (now merged), and [a subsequent release](https://github.com/pygments/pygments/milestone/23)
This is taken from https://github.com/leanprover/lean4/blob/d92948bc20b12f53542814c79469711ceff19fbf/doc/latex/lean4.py, with subsequent commits showing the changes made on top of this file
For that reason, I'd prefer if the history could be preserved; though I'd be happy to rewrite it if you want fewer commits / different message conventions.
The test file I'd added is the lean4 translation of the test file that was being used for Lean 3.
Since lean3 and lean4 files share a file extension, this adds
analyse_text
methods that discriminate based onimport Foo
vsimport foo
; this is the same heuristic used by GitHub linguist.cc @Kha