Skip to content
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.

Sign up for GitHub

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

Jump to bottom

initial support for lean 3 #1798

Merged
merged 4 commits into from Mar 5, 2022
Merged

initial support for lean 3 #1798

merged 4 commits into from Mar 5, 2022

Conversation

kunigami
Copy link
Contributor

I'd like to add support to lean 3 (https://leanprover-community.github.io). I followed the instruction in
https://rouge-ruby.github.io/docs/file.LexerDevelopment.html

Verified that

bundle exec rake

runs without errors and did a visual check at http://localhost:9292/lean

@hrldcpr hrldcpr mentioned this pull request Jan 31, 2022
Closed
@hrldcpr
Copy link

hrldcpr commented Feb 1, 2022

Thanks for this!

I think you should add inductive, Prop, and #reduce as keywords (they're all highlighted as keywords in both the Lean web editor and VS Code)

@hrldcpr
Copy link

hrldcpr commented Feb 1, 2022 •
edited

Also in case anyone else is hoping to use this in Jekyll before it's merged but is a ruby noob like me, you can add this line to your Gemfile:

gem "rouge", git: "https://github.com/kunigami/rouge", branch: "lean"

and then run bundle install

@tancnle tancnle added the needs-review The PR needs to be reviewed label Feb 1, 2022
@kunigami
Copy link
Contributor Author

kunigami commented Feb 1, 2022

Thanks! Will do, the commit you linked also seems more complete in keyword + operators coverage. I can look into adding them (I'm quite new to Lean, so happy to go figure out examples for the other keywords).

tancnle
tancnle reviewed Mar 3, 2022
View reviewed changes
Copy link
Collaborator

@tancnle tancnle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for your contribution @kunigami ❤️ The PR looks good overall. I have left some suggestions. Please let me know what you think 🙏🏼

lib/rouge/lexers/lean.rb Show resolved Hide resolved
lib/rouge/lexers/lean.rb Show resolved Hide resolved
lib/rouge/lexers/lean.rb Outdated Show resolved Hide resolved
lib/rouge/lexers/lean.rb Show resolved Hide resolved
@tancnle tancnle added author-action The PR has been reviewed but action by the author is needed and removed needs-review The PR needs to be reviewed labels Mar 3, 2022
@hrldcpr
Copy link

hrldcpr commented Mar 4, 2022

Can you add inductive, Prop, and #reduce as keywords? (They're considered keywords in both the Lean web editor and VS Code)

@tancnle
Copy link
Collaborator

tancnle commented Mar 5, 2022

Thank you for your hard work @kunigami 🙇🏼 The PR looks great to me 🚀

@tancnle tancnle merged commit 776cbc4 into rouge-ruby:master Mar 5, 2022
@kunigami
Copy link
Contributor Author

kunigami commented Mar 5, 2022

Yay! Thanks for the review and support, @tancnle !

@tancnle tancnle removed the author-action The PR has been reviewed but action by the author is needed label Mar 5, 2022
razetime pushed a commit to razetime/rouge that referenced this pull request Jun 30, 2022
@kunigami @razetime
initial support for lean 3 (rouge-ruby#1798)
14cea0a 
* initial support for lean 3

* incorporate keywords and operators from PR rouge-ruby#1019

* address comments

* add keyword::type + other keywords
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tancnle tancnle tancnle left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@kunigami @hrldcpr @tancnle