Skip to content

Conversation

@grunweg
Copy link
Contributor

@grunweg grunweg commented Jan 14, 2026

This PR makes the pretty-printing of class abbrev syntax match its doc-string. The previous output was missing lots of intermediate spaces.

Found by using the pretty-printer for formatting linting in leanprover-community/mathlib4#30658.

Let me test this change first before asking for review.

@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 Jan 14, 2026
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-14 17:01:43)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-14 17:01:44)

@nomeata
Copy link
Collaborator

nomeata commented Jan 14, 2026

Let me test this change first before asking for review.

I recommend to use the draft PR feature whenever you don't want people to look or merge yet

@grunweg grunweg marked this pull request as draft January 14, 2026 21:22
This PR makes the pretty-printing of class abbrev syntax match its doc-string.
The previous output was missing lots of intermediate spaces.

Found by using the pretty-printer for formatting linting in
leanprover-community/mathlib4#30658.
@grunweg
Copy link
Contributor Author

grunweg commented Jan 14, 2026

Let's hope this attempt works: I'd like to get a branch of mathlib, so I can test the pretty-printing there...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants