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

doc: upstream the Lean4 pygments lexer #3125

Merged
merged 5 commits into from
May 20, 2024
Merged

doc: upstream the Lean4 pygments lexer #3125

merged 5 commits into from
May 20, 2024

Conversation

eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Dec 30, 2023 •
edited

An improved lean4 lexer is now part of pygments.

This depends on pygments/pygments#2618 (now merged), and a subsequent release

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 30, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 30, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3125
f745fcc
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 30, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

  • ✅ Mathlib branch lean-pr-testing-3125 has successfully built against this PR. (2023-12-30 20:13:37) View Log
  • ✅ Mathlib branch lean-pr-testing-3125 has successfully built against this PR. (2023-12-30 20:47:09) View Log
  • ✅ Mathlib branch lean-pr-testing-3125 has successfully built against this PR. (2024-01-14 15:52:14) View Log
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-05-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-05-19 22:34:56)

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 30, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3125
dc8192b
@eric-wieser eric-wieser changed the title Upstream the Lean4 pygments lexer doc: upstream the Lean4 pygments lexer Dec 30, 2023
@eric-wieser eric-wieser marked this pull request as ready for review January 14, 2024 14:17
@eric-wieser
Copy link
Contributor Author

This isn't quite ready to be merged (as Pygments 2.18 is not yet released), but the new instructions already work against a development install of pygments.

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 14, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3125
7f8a107
@semorrison semorrison marked this pull request as draft January 14, 2024 23:53
@semorrison
Copy link
Collaborator

Marking as draft until Pygments 2.18 is released.

@eric-wieser eric-wieser mentioned this pull request Feb 12, 2024
Open
@eric-wieser eric-wieser marked this pull request as ready for review May 5, 2024 21:56
@eric-wieser
Copy link
Contributor Author

Pygments has now released: https://github.com/pygments/pygments/blob/master/CHANGES

@semorrison
Copy link
Collaborator

Thanks! If you could rebase or merge master, hopefully CI will go through and we can merge.

@eric-wieser
Copy link
Contributor Author

Master is now merged

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label May 19, 2024
@semorrison semorrison removed the awaiting-review Waiting for someone to review the PR label May 20, 2024
@semorrison semorrison added this pull request to the merge queue May 20, 2024
Merged via the queue into leanprover:master with commit f0471a5 May 20, 2024
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@eric-wieser @leanprover-community-mathlib4-bot @semorrison