Skip to content

fix: behavior of hard line breaks in Format strings #8457

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
jrr6 merged 2 commits into from
May 29, 2025
Merged

fix: behavior of hard line breaks in Format strings #8457

jrr6 merged 2 commits into from
May 29, 2025

Conversation

@jrr6
Copy link
Contributor

@jrr6 jrr6 commented May 23, 2025

This PR fixes an issue when including a hard line break in a Format that caused subsequent (ordinary) line breaks to be erroneously flattened to spaces.

This issue is especially important for displaying notes and hints in error messages, as these components could appear garbled due to improper line-break rendering.

@jrr6 jrr6 added the changelog-pp Pretty printing label May 23, 2025
@jrr6 jrr6 requested a review from kim-em as a code owner May 23, 2025 20:38
@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 May 23, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8457
57164ce
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8457
dca8694
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 23, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 23, 2025 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 23, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8457
68202d0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8457
1b0a03f
@jrr6 jrr6 requested a review from nomeata May 24, 2025 01:36
@nomeata
Copy link
Collaborator

nomeata commented May 26, 2025

@Vtec234, I see you had workd on this module before. Could I tempt you to have a look?

@nomeata nomeata requested a review from Vtec234 May 26, 2025 10:22
@jrr6 jrr6 mentioned this pull request May 26, 2025
Merged
@jrr6 jrr6 added this pull request to the merge queue May 29, 2025
@jrr6
Copy link
Contributor Author

jrr6 commented May 29, 2025

Merging this now to fix hint rendering before the next RC. This can be revisited if the implementation needs adjusting.

Merged via the queue into leanprover:master with commit 020da5b May 29, 2025
15 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Jun 1, 2025
@jrr6
fix: improve error-message hint rendering and API (#8486)
43aec5b 
This PR improves the rendering of hints in error messages by
consistently indenting diffs and splitting large diffs less granularly;
it also improves the ergonomics of `Lean.MessageData.hint`. Note that
the changes to the signature of `Lean.MessageData.hint` are breaking.

This PR depends on #8457.
jcommelin pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025
@leanprover-community-mathlib4-bot @kim-em
@Vierkantor @Kha @eric-wieser @Rob23oba @jrr6
chore: adaptations for nightly-2025-06-04 (#25431)
3780f5f 
* Update lean-toolchain for testing leanprover/lean4#8347

* fixes for leanprover/lean4#8347

* Update lean-toolchain for testing leanprover/lean4#8397

* deprecations for leanprover/lean4#8397

* chore: bump to nightly-2025-05-19

* chore: adaptations for nightly-2025-05-19

* Trigger CI for leanprover/lean4#8347

* Update the style linter to use LinterOptions

* Fix test

* chore: adaptations for nightly-2025-05-19 (#25017)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>

* chore: bump to nightly-2025-05-20

* Merge master into nightly-testing

* feat: a `grind` test case (#25037)

Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test.

Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.)

* lake update

* fixes

* fixes

* fixes

* fixes

* fix

* fixes

* fixes

* shake --update

* chore: bump to nightly-2025-05-21

* Update lean-toolchain for testing leanprover/lean4#7352

* lake update

* Trigger CI for leanprover/lean4#7352

* chore: adaptations for nightly-2025-05-21

* chore: adaptations for nightly-2025-05-21 (#25079)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>

* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#8584

* chore: adaptations for nightly-2025-06-02

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* chore: bump to nightly-2025-06-04

* bump toolchain

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>
jcommelin added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2025
@leanprover-community-mathlib4-bot @kim-em
@eric-wieser @Rob23oba @jrr6 @Vierkantor @Kha @jcommelin @JovanGerb @nomeata
chore: adaptations for nightly-2025-06-05 (#25490)
5a9a408 
* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

* Update lean-toolchain for testing leanprover/lean4#8519

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* Trigger CI for leanprover/lean4#8519

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* chore: remove simp attribute when value of argument can not be inferred by simp

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#8584

* chore: adaptations for nightly-2025-06-02

* change phrasing of comments

* chore(Geometry/Manifold): two simp-lemmas can be proven by simp

* fix two lint problems

* Trigger CI for leanprover/lean4#8519

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* revert change in `Mathlib.Data.ZMOD.Basic`

* fix Mathlib/Data/List/EditDistance/Estimator.lean

* give specialized simp lemmas higher prio

* simp can prove these

* simp can prove these

* chore: bump to nightly-2025-06-04

* bump toolchain

* Adapt eqns

* Revert "Adapt eqns"

This reverts commit 34f1f7f.

* Simply remove check for now

* fix a bunch

* fixes?

* chore: adaptations for nightly-2025-06-04

* add `simp low` lemma `injOn_of_eq_iff_eq`

* wip

* wip

* wip

* fix

* Trigger CI for leanprover-community/batteries#1220

* Merge master into nightly-testing

* chore: bump to nightly-2025-06-05

* Kick CI

* Bump lean4-cli

* Bump import-graph

* Kick CI

* update lakefile

* chore: use more robust syntax quotation in Shake

* cleanup lakefile

---------

Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@nomeata nomeata Awaiting requested review from nomeata

@Vtec234 Vtec234 Awaiting requested review from Vtec234

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-pp Pretty printing 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

@jrr6 @leanprover-community-bot @nomeata