Skip to content

chore: warn about visibility on unnamed initializers - #14586

Merged
Vtec234 merged 3 commits into
masterfrom
meta-init-vis
Jul 29, 2026
Merged

chore: warn about visibility on unnamed initializers#14586
Vtec234 merged 3 commits into
masterfrom
meta-init-vis

Conversation

@Vtec234

@Vtec234 Vtec234 commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR warns about public/private visibility modifiers on unnamed initialize blocks - they do not do anything which can be confusing.

@Vtec234 Vtec234 added the changelog-language Language features and metaprograms label Jul 29, 2026
@Vtec234 Vtec234 mentioned this pull request Jul 29, 2026
Open
3 tasks
@Vtec234
Vtec234 requested a review from Kha July 29, 2026 02:29
@Vtec234 Vtec234 changed the title chore: prohibit visibility on unnamed initializers chore: warn about visibility on unnamed initializers Jul 29, 2026
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Jul 29, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jul 29, 2026
@leanprover-bot

leanprover-bot commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14586
ad3205a
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14586
746fc5d
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 29, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14586
c3fbb17
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jul 29, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

Kha
Kha approved these changes Jul 29, 2026
View reviewed changes

@Kha Kha left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@Vtec234
Vtec234 added this pull request to the merge queue Jul 29, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Jul 29, 2026
@Vtec234
Vtec234 requested a review from tydeu as a code owner July 29, 2026 18:55
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14586
77c29b0
@Vtec234
Vtec234 added this pull request to the merge queue Jul 29, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14586
fa94260
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 29, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14586
0678772
Merged via the queue into master with commit f696c46 Jul 29, 2026
20 checks passed
@Vtec234
Vtec234 deleted the meta-init-vis branch July 29, 2026 20:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha approved these changes
@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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

@Vtec234 @leanprover-bot @Kha