Skip to content

chore: use backticks for sorry in diagnostic messages#11608

Merged
nomeata merged 1 commit intoleanprover:masterfrom
alok:sorry-backtick-warning
Dec 15, 2025
Merged

chore: use backticks for sorry in diagnostic messages#11608
nomeata merged 1 commit intoleanprover:masterfrom
alok:sorry-backtick-warning

Conversation

@alok
Copy link
Contributor

@alok alok commented Dec 11, 2025 •
edited by nomeata
Loading

This PR changes the "declaration uses 'sorry'" warning to use backticks instead of single quotes, consistent with Lean's conventions for formatting code identifiers in diagnostic messages.

@alok
chore: use backticks for sorry in diagnostic messages
2f26634 
This PR changes the "declaration uses 'sorry'" warning to use backticks
(`sorry`) instead of single quotes ('sorry'), consistent with Lean's
conventions for formatting code identifiers in diagnostic messages.
@alok alok force-pushed the sorry-backtick-warning branch from 92dede8 to 2f26634 Compare December 15, 2025 12:19
@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 15, 2025
@ghost
Copy link

ghost commented Dec 15, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9b49b6b68daa8b7a2da6575b0783bf3b6de34adb --onto 6a0b0c8273ab560d093494a2daa4dd3088437ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-15 13:23:19)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 15, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9b49b6b68daa8b7a2da6575b0783bf3b6de34adb --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-15 13:23:20)

@nomeata nomeata enabled auto-merge December 15, 2025 14:30
@nomeata nomeata added this pull request to the merge queue Dec 15, 2025
Merged via the queue into leanprover:master with commit 949cf69 Dec 15, 2025
19 checks passed
nomeata added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 16, 2025
@nomeata
Adapt to leanprover/lean4#11608
70f9a3a
nomeata added a commit to nomeata/aesop that referenced this pull request Dec 16, 2025
@nomeata
Adapt to leanprover/lean4#11608
bd9c6ee
kim-em pushed a commit to leanprover-community/aesop that referenced this pull request Dec 16, 2025
@nomeata
Adapt to leanprover/lean4#11608 (#302)
33c0b1e
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 26, 2026
@kim-em @nomeata
@Kha @Ruben-VandeVelde @leanprover-community-bot-assistant @claude @kbuzzard @Rob23oba @TwoFX
chore: bump toolchain to v4.28.0-rc1 (#34436)
5352afc 
* deprecation in lakefile

* chore: bump to nightly-2025-12-10

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

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

* chore: adaptations for nightly-2025-12-10

* fix

* fix for leanprover/lean4#11581

* deprecation

* remove unused argument

* feat: register mathlib tactics with try? (#136)

This PR adds `register_try?_tactic` calls for all finishing tactics currently registered with `register_hint`, which are not already covered by `grind` modules (i.e. I have not registered `linarith` or `ring`), using identical priority values:

**Common tactics** (Common.lean):
- tauto (priority 500)
- aesop (priority 80)
- fun_prop (priority 200)

**Domain-specific tactics**:
- norm_num (1000), noncomm_ring (1000)
- field (850), bound (70)
- finiteness (1000), compute_degree (1000), positivity (1000), field_simp (1000)


🤖 Prepared with Claude Code

* chore: adaptations for nightly-2025-12-10 (#141)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* fix deprecation in mk_all

* chore: adaptations for nightly-2025-12-10

* chore: bump to nightly-2025-12-11

* Kick CI

* lake update

* fix deps

* remove upstreamed

* workaround

* fix

* chore: bump to nightly-2025-12-12

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

* more fix

* fix the fix

* lake update

* adding a prime to NameMapExtension

* adaptations for leanprover/lean4#11620

* revert spurious change

* warning

* Merge master into nightly-testing

* fixes

* fix

* deprecations

* chore: bump to nightly-2025-12-13

* lake update

* lake update

* fix merge

* revert a lia back to omega

* remove upstreamed

* deprecation

* fixes

* fix archive

* lint

* lake update aesop

* chore: adaptations for nightly-2025-12-13

* remove aliases for upstreamed lemmas

* deprecation

* revert a lia back to omega

* lake update

* cutsat to lia

* hm

* note

* adaptation notes

* chore: bump to nightly-2025-12-14

* remove @[grind =] from even_sign_iff

* chore: adaptations for nightly-2025-12-13 (#142)

* lake update

* chore: adaptations for nightly-2025-12-14 (#143)

* chore: adaptations for nightly-2025-12-14

* chore: update lean-toolchain to leanprover/lean4:nightly-2025-12-14

* chore: bump to nightly-2025-12-15

* chore: adaptations for nightly-2025-12-15 (#144)

* chore: bump to nightly-2025-12-16

* Update batteries

* Adapt to leanprover/lean4#11608

* Pull in aesop fixes (from my fork, sorry for that)

* chore: adaptations for nightly-2025-12-16

* fixes

* chore: bump to nightly-2025-12-17

* chore: adaptations for nightly-2025-12-17

* chore: adaptations for nightly-2025-12-16 (#145)

* chore: adaptations for nightly-2025-12-17 (#146)

* chore: adaptations for nightly-2025-12-17

* chore: bump to nightly-2025-12-18

* lake update

* chore: adaptations for nightly-2025-12-18

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

* remove upstreamed

* remove upstreamed

* fixes

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

* mk_all

* chore: adaptations for nightly-2025-12-20

* chore: adaptations for nightly-2025-12-20 (#148)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* chore: adaptations for nightly-2025-12-20

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

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

* chore: adaptations for nightly-2025-12-21 (#149)

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

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

* chore: adaptations for nightly-2025-12-22

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

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

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

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

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

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

* chore: adaptations for nightly-2025-12-26

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

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

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

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

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

* chore: bump to nightly-2026-01-01

* chore: bump to nightly-2026-01-02

* lake update

* chore: bump to nightly-2026-01-03

* chore: bump to nightly-2026-01-04

* merge lean-pr-testing-10059

* lake update

* deprecations

* Revert "merge lean-pr-testing-10387"

This reverts commit e166d33, reversing
changes made to cf6049c.

* fix

* Revert incorrectly merged lean-pr-testing branches

Reverts the following branches that were incorrectly merged due to a bug
in discover-lean-pr-testing.yml where an empty prs.txt caused grep to
match ALL lean-pr-testing branches:

- lean-pr-testing-2714 (from Oct 2023!)
- lean-pr-testing-11455
- lean-pr-testing-11163
- lean-pr-testing-10231
- lean-pr-testing-10178
- lean-pr-testing-10059

These PRs are not in nightly-2026-01-04, so their adaptations should not
be merged.

The bug fix is in: #33546

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* deprecations

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

* fix

* chore: bump to nightly-2026-01-05

* remove upstreamed

* lake update

* fix

* chore: adaptations for nightly-2026-01-05

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

* chore: adaptations for nightly-2026-01-06

* chore: adaptations for nightly-2026-01-06

* chore: bump to nightly-2026-01-07

* chore: adaptations for nightly-2026-01-07

* chore: adaptations for nightly-2026-01-09 (#159)

* replace aesop proof

* chore: adaptations for nightly-2026-01-07

* chore: bump to nightly-2026-01-08

* chore: adaptations for nightly-2026-01-08

* chore: bump to nightly-2026-01-09

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

* chore: adaptations for nightly-2026-01-23 (#160)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2026-01-24 (#161)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2026-01-25 (#162)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: bump toolchain to v4.28.0-rc1

* fix: use main/master instead of nightly-testing for dependencies

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: leanprover-community-bot-assistant <97194829+leanprover-community-bot-assistant@users.noreply.github.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
YellPika pushed a commit to YellPika/mathlib4 that referenced this pull request Feb 3, 2026
@kim-em @nomeata
@Kha @Ruben-VandeVelde @leanprover-community-bot-assistant @claude @kbuzzard @Rob23oba @TwoFX @YellPika
chore: bump toolchain to v4.28.0-rc1 (leanprover-community#34436)
d2ed69f 
* deprecation in lakefile

* chore: bump to nightly-2025-12-10

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

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

* chore: adaptations for nightly-2025-12-10

* fix

* fix for leanprover/lean4#11581

* deprecation

* remove unused argument

* feat: register mathlib tactics with try? (leanprover-community#136)

This PR adds `register_try?_tactic` calls for all finishing tactics currently registered with `register_hint`, which are not already covered by `grind` modules (i.e. I have not registered `linarith` or `ring`), using identical priority values:

**Common tactics** (Common.lean):
- tauto (priority 500)
- aesop (priority 80)
- fun_prop (priority 200)

**Domain-specific tactics**:
- norm_num (1000), noncomm_ring (1000)
- field (850), bound (70)
- finiteness (1000), compute_degree (1000), positivity (1000), field_simp (1000)


🤖 Prepared with Claude Code

* chore: adaptations for nightly-2025-12-10 (leanprover-community#141)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* fix deprecation in mk_all

* chore: adaptations for nightly-2025-12-10

* chore: bump to nightly-2025-12-11

* Kick CI

* lake update

* fix deps

* remove upstreamed

* workaround

* fix

* chore: bump to nightly-2025-12-12

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

* more fix

* fix the fix

* lake update

* adding a prime to NameMapExtension

* adaptations for leanprover/lean4#11620

* revert spurious change

* warning

* Merge master into nightly-testing

* fixes

* fix

* deprecations

* chore: bump to nightly-2025-12-13

* lake update

* lake update

* fix merge

* revert a lia back to omega

* remove upstreamed

* deprecation

* fixes

* fix archive

* lint

* lake update aesop

* chore: adaptations for nightly-2025-12-13

* remove aliases for upstreamed lemmas

* deprecation

* revert a lia back to omega

* lake update

* cutsat to lia

* hm

* note

* adaptation notes

* chore: bump to nightly-2025-12-14

* remove @[grind =] from even_sign_iff

* chore: adaptations for nightly-2025-12-13 (leanprover-community#142)

* lake update

* chore: adaptations for nightly-2025-12-14 (leanprover-community#143)

* chore: adaptations for nightly-2025-12-14

* chore: update lean-toolchain to leanprover/lean4:nightly-2025-12-14

* chore: bump to nightly-2025-12-15

* chore: adaptations for nightly-2025-12-15 (leanprover-community#144)

* chore: bump to nightly-2025-12-16

* Update batteries

* Adapt to leanprover/lean4#11608

* Pull in aesop fixes (from my fork, sorry for that)

* chore: adaptations for nightly-2025-12-16

* fixes

* chore: bump to nightly-2025-12-17

* chore: adaptations for nightly-2025-12-17

* chore: adaptations for nightly-2025-12-16 (leanprover-community#145)

* chore: adaptations for nightly-2025-12-17 (leanprover-community#146)

* chore: adaptations for nightly-2025-12-17

* chore: bump to nightly-2025-12-18

* lake update

* chore: adaptations for nightly-2025-12-18

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

* remove upstreamed

* remove upstreamed

* fixes

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

* mk_all

* chore: adaptations for nightly-2025-12-20

* chore: adaptations for nightly-2025-12-20 (leanprover-community#148)



Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* chore: adaptations for nightly-2025-12-20

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

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

* chore: adaptations for nightly-2025-12-21 (leanprover-community#149)

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

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

* chore: adaptations for nightly-2025-12-22

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

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

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

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

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

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

* chore: adaptations for nightly-2025-12-26

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

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

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

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

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

* chore: bump to nightly-2026-01-01

* chore: bump to nightly-2026-01-02

* lake update

* chore: bump to nightly-2026-01-03

* chore: bump to nightly-2026-01-04

* merge lean-pr-testing-10059

* lake update

* deprecations

* Revert "merge lean-pr-testing-10387"

This reverts commit e166d33, reversing
changes made to cf6049c.

* fix

* Revert incorrectly merged lean-pr-testing branches

Reverts the following branches that were incorrectly merged due to a bug
in discover-lean-pr-testing.yml where an empty prs.txt caused grep to
match ALL lean-pr-testing branches:

- lean-pr-testing-2714 (from Oct 2023!)
- lean-pr-testing-11455
- lean-pr-testing-11163
- lean-pr-testing-10231
- lean-pr-testing-10178
- lean-pr-testing-10059

These PRs are not in nightly-2026-01-04, so their adaptations should not
be merged.

The bug fix is in: leanprover-community#33546

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* deprecations

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

* fix

* chore: bump to nightly-2026-01-05

* remove upstreamed

* lake update

* fix

* chore: adaptations for nightly-2026-01-05

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

* chore: adaptations for nightly-2026-01-06

* chore: adaptations for nightly-2026-01-06

* chore: bump to nightly-2026-01-07

* chore: adaptations for nightly-2026-01-07

* chore: adaptations for nightly-2026-01-09 (leanprover-community#159)

* replace aesop proof

* chore: adaptations for nightly-2026-01-07

* chore: bump to nightly-2026-01-08

* chore: adaptations for nightly-2026-01-08

* chore: bump to nightly-2026-01-09

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

* chore: adaptations for nightly-2026-01-23 (leanprover-community#160)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2026-01-24 (leanprover-community#161)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2026-01-25 (leanprover-community#162)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: bump toolchain to v4.28.0-rc1

* fix: use main/master instead of nightly-testing for dependencies

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: leanprover-community-bot-assistant <97194829+leanprover-community-bot-assistant@users.noreply.github.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Rob23oba <robin@arnez.web.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
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

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

@alok @leanprover-bot @nomeata