Skip to content

feat: deriving instances: use accessible names#10271

Merged
nomeata merged 4 commits intomasterfrom
joachim/accessible-names
Sep 6, 2025
Merged

feat: deriving instances: use accessible names#10271
nomeata merged 4 commits intomasterfrom
joachim/accessible-names

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Sep 6, 2025 •
edited
Loading

This PR changes the naming of the internal functions in deriving instances like BEq to use accessible names. This is necessary to reasonably easily prove things about these functions. For example after deriving BEq for a type T, the implementation of instBEqT is in instBEqT.beq.

@nomeata nomeata added the changelog-language Language features and metaprograms label Sep 6, 2025
@nomeata nomeata mentioned this pull request Sep 6, 2025
Closed
@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 Sep 6, 2025
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 6, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-05 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. (2025-09-06 12:33:49)

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Sep 6, 2025
Update lean-toolchain for testing leanprover/lean4#10271
2c1ff56
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 6, 2025
Update lean-toolchain for testing leanprover/lean4#10271
e66a093
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Sep 6, 2025
@ghost
Copy link
Copy Markdown

ghost commented Sep 6, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

nomeata added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 6, 2025
@nomeata
Adapt to leanprover/lean4#10271
ac854de
@nomeata nomeata marked this pull request as ready for review September 6, 2025 15:26
@nomeata nomeata requested a review from kim-em as a code owner September 6, 2025 15:26
@nomeata nomeata added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Sep 6, 2025
@nomeata nomeata enabled auto-merge September 6, 2025 15:27
@ghost ghost removed awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Sep 6, 2025
@ghost
Copy link
Copy Markdown

ghost commented Sep 6, 2025

@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 6, 2025
@nomeata nomeata added this pull request to the merge queue Sep 6, 2025
@nomeata nomeata removed this pull request from the merge queue due to a manual request Sep 6, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Sep 6, 2025
Update lean-toolchain for leanprover/lean4#10271
68059a8
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 6, 2025
Update lean-toolchain for leanprover/lean4#10271
2a4c571
@nomeata nomeata mentioned this pull request Sep 6, 2025
Merged
@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Sep 6, 2025

Hmm, this triggers mathlib linters that previously ignored the inaccessible definition. But running out steam to proactively fix those, sorry.

@nomeata nomeata added this pull request to the merge queue Sep 6, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Sep 6, 2025
@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Sep 6, 2025

I left the name that was there, but you are right, now that it's more visible this should be beq.

@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Sep 6, 2025

Ah, it is beq, I just typo’ed the description.

@nomeata nomeata enabled auto-merge September 6, 2025 18:00
@nomeata nomeata added this pull request to the merge queue Sep 6, 2025
Merged via the queue into master with commit 316ff35 Sep 6, 2025
14 checks passed
@nomeata nomeata mentioned this pull request Sep 8, 2025
Open
kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 15, 2025
@leanprover-community-bot-assistant @Rob23oba
@kim-em @Vierkantor @tydeu @datokrat @nomeata @kmill
chore: adaptations for nightly-2025-09-15 (#63)
4244037 
* fix deprecations

* remove upstreamed defs

* two fixes

* fix merge

* fix merge

* revert sqrt changes

* ugh

* fix from nightly-testing

* fix merge

* remove test deleted on master

* fix test

* note about test

* .

* Update lean-toolchain for leanprover/lean4#10194

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

* adjust to upstream changes

* fix

* fix

* long line

* Use Mathlib's nightly toolchain to run docgen in the nightly test

* simpNF linter

* whitespace

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

* Correct the working directory: should be 'docbuild'

* Rework the grind regression report as a nightly-testing regression report

It should still report the same things, but now as one message for all regression kinds

* feat(Cache): download speeds & more info on errors

* fix(Cache): add base download failure message

* fixes

* turn off linter

* adaptation note

* turn off linter.nightlyRegressionSet

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

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

* Update lean-toolchain for leanprover/lean4#10217

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

* Remove the erroring nightly regression report, we'll develop this on another branch.

* fixes

* update LibraryRewrite test

* Update lean-toolchain for leanprover/lean4#10059

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

* fix

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

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

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

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

* Adapt to leanprover/lean4#10271

* Bump batteries

* Update lean-toolchain for leanprover/lean4#10271

* chore: bump to nightly-2025-09-07

* nolint unusedArguments

* Merge master into nightly-testing

* chore: bump to nightly-2025-09-08

* fixes

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

* fix thing

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

* temporarily remove test

* adaptation note

* master version of Cache/Requests.lean

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

* adaptation note

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

* merge lean-pr-testing-10059

* bump toolchain manually??

* restore test

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

* lake update

* fix

* adaptations for leanprover/lean4#10307

* remove validateDocComment in ToAdditive

* remove upstreamed Function.Injective

* update assert_not_exists

* oops

* comment out DeriveTraversable

* chore: replace some grind attibutes with grind_pattern, to be robust for future heuristic changes

* suggestions from Rob23oba

* lshake --fix

* fix bad shake

* shake --update

* .

* chore: adaptations for nightly-2025-09-11

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

* Revert "oops"

This reverts commit 517b832.

* Revert "comment out DeriveTraversable"

This reverts commit 0460eb8.

* fix DeriveTraversable

* add `binders` fields

* fix

* fixes

* update manifest

* fixes

* fixes

* fixes

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

* fixes

* fixes

* fixes

* fixes

* fixes

* fixes

* fixes

* remove adaptation note

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

* fixes

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

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

* fix

* fix

* fix

* fix emrge

* update batteries

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

* Merge master into nightly-testing

* Update Mathlib/Data/List/Basic.lean

* Merge master into nightly-testing

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

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

---------

Co-authored-by: Rob23oba <robin.arnez@web.de>
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: github-actions <github-actions@github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
@nomeata nomeata mentioned this pull request Sep 16, 2025
Closed
@nomeata nomeata mentioned this pull request Oct 6, 2025
Closed
3 tasks
nomeata added a commit that referenced this pull request Oct 6, 2025
@nomeata
fix: instance name for deriving ToExpr
2046632 
This PR changes the instance name for `deriving ToExpr` to be consistent
with other derived instance since #10271. Fixes #10678.
@nomeata nomeata mentioned this pull request Oct 6, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Oct 6, 2025
@nomeata
fix: instance name for deriving ToExpr (#10682)
30f41fe 
This PR changes the instance name for `deriving ToExpr` to be consistent
with other derived instance since #10271. Fixes #10678.
arthur-adjedj pushed a commit to arthur-adjedj/lean4 that referenced this pull request Oct 6, 2025
@nomeata @arthur-adjedj
fix: instance name for deriving ToExpr (leanprover#10682)
052b2bf 
This PR changes the instance name for `deriving ToExpr` to be consistent
with other derived instance since leanprover#10271. Fixes leanprover#10678.
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

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms 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.

2 participants

@nomeata @leanprover-bot