Skip to content

doc: upstream the Lean4 pygments lexer #3125

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
Merged
kim-em merged 5 commits into from
May 20, 2024
Merged

doc: upstream the Lean4 pygments lexer #3125

kim-em merged 5 commits into from
May 20, 2024

Conversation

@eric-wieser
Copy link
Contributor

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

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

leanprover-community-mathlib4-bot commented Dec 30, 2023 •
edited
Loading

  • ✅ 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

eric-wieser commented Jan 14, 2024

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
@kim-em kim-em marked this pull request as draft January 14, 2024 23:53
@kim-em
Copy link
Collaborator

kim-em commented Jan 14, 2024

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

eric-wieser commented May 5, 2024

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

@kim-em
Copy link
Collaborator

kim-em commented May 6, 2024

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

@eric-wieser
Copy link
Contributor Author

eric-wieser commented May 19, 2024

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
@kim-em kim-em removed the awaiting-review Waiting for someone to review the PR label May 20, 2024
@kim-em kim-em added this pull request to the merge queue May 20, 2024
Merged via the queue into leanprover:master with commit f0471a5 May 20, 2024
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.

3 participants

@eric-wieser @leanprover-community-mathlib4-bot @kim-em