Skip to content

fix: respect visibility in initialize/builtin_initialize#13239

Merged
leanprover-bot merged 3 commits intoleanprover:masterfrom
Kha:push-nmumxwnsszso
Apr 10, 2026
Merged

fix: respect visibility in initialize/builtin_initialize#13239
leanprover-bot merged 3 commits intoleanprover:masterfrom
Kha:push-nmumxwnsszso

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Apr 1, 2026

This PR fixes an issue where (builtin_)initialize inside module would not allow referencing private defs in its type unless explicitly prefixed with private.

@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 Apr 1, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 1, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-25 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-04-01 17:58:32)
  • ✅ Reference manual branch lean-pr-testing-13239 has successfully built against this PR. (2026-04-02 12:57:34) View Log
  • 🟡 Reference manual branch lean-pr-testing-13239 build against this PR didn't complete normally. (2026-04-02 12:58:17) View Log
  • ✅ Reference manual branch lean-pr-testing-13239 has successfully built against this PR. (2026-04-07 10:22:31) View Log
  • 🟡 Reference manual branch lean-pr-testing-13239 build against this PR didn't complete normally. (2026-04-07 10:24:19) View Log
  • ✅ Reference manual branch lean-pr-testing-13239 has successfully built against this PR. (2026-04-09 14:51:00) View Log
  • 🟡 Reference manual branch lean-pr-testing-13239 build against this PR didn't complete normally. (2026-04-09 14:54:02) View Log
  • ✅ Reference manual branch lean-pr-testing-13239 has successfully built against this PR. (2026-04-09 17:19:18) View Log
  • 🟡 Reference manual branch lean-pr-testing-13239 build against this PR didn't complete normally. (2026-04-09 17:21:20) View Log
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-07 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-04-10 11:36:50)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026
Update lean-toolchain for testing leanprover/lean4#13239
91d8740
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 1, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026
Update lean-toolchain for testing leanprover/lean4#13239
60cd6a6
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 1, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 1, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-nmumxwnsszso branch from d16b7cc to 20adc72 Compare April 2, 2026 11:45
@Kha Kha added the changelog-language Language features and metaprograms label Apr 2, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2026
Update lean-toolchain for leanprover/lean4#13239
eac9bcd
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 2, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#13239
a98b3a8
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 2, 2026
Update lean-toolchain for leanprover/lean4#13239
0f3cc0a
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Apr 2, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 2, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-nmumxwnsszso branch from 20adc72 to 44820fe Compare April 7, 2026 09:10
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 7, 2026
Update lean-toolchain for leanprover/lean4#13239
1536abc
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 7, 2026
Update lean-toolchain for leanprover/lean4#13239
e39e2f7
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 7, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13239
55fc8f9
@mathlib-lean-pr-testing mathlib-lean-pr-testing 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 Apr 7, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 7, 2026

Mathlib CI status (docs):

@Kha Kha added this pull request to the merge queue Apr 8, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 8, 2026
@Kha Kha force-pushed the push-nmumxwnsszso branch from 44820fe to 9bcc69d Compare April 9, 2026 13:37
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2026
Update lean-toolchain for leanprover/lean4#13239
07de1f0
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 9, 2026
Update lean-toolchain for leanprover/lean4#13239
c461780
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 9, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13239
4bb6a4b
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Apr 9, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 9, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-nmumxwnsszso branch from 9bcc69d to 5cf76f0 Compare April 9, 2026 16:05
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2026
Update lean-toolchain for leanprover/lean4#13239
8dc84fc
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 9, 2026
Update lean-toolchain for leanprover/lean4#13239
6d7623d
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 9, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13239
c0c81cb
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 9, 2026

Mathlib CI status (docs):

@Kha Kha changed the base branch from master to nightly-with-mathlib April 10, 2026 10:31
@Kha Kha changed the title fix: respect visibility in initialize/builtin_initialize [REBASED] fix: respect visibility in initialize/builtin_initialize Apr 10, 2026
@Kha Kha force-pushed the push-nmumxwnsszso branch from 5cf76f0 to 4013a04 Compare April 10, 2026 10:38
@Kha Kha requested review from hargoniX and leodemoura as code owners April 10, 2026 10:38
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13239
b13caf6
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13239
db18a79
Kha added 2 commits April 10, 2026 11:46
@Kha
fix: respect module visibility in initialize/builtin_initialize
40fb619 
Previously, `elabInitialize` only checked for explicit `private` when
deciding whether to mangle `fullId`, ignoring the `module` system's
default-private semantics. It also overrode the user's visibility for
the generated `initFn` via `visibility.ofBool`.

Now, `elabInitialize` uses `elabVisibility` + `isInferredPublic` to
correctly handle all visibility contexts. The generated `initFn`
inherits the user's visibility rather than being forced public.

Also factors out `elabVisibility` from `elabModifiers` for reuse.
@Kha
chore: update stage0
720ae83
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-nmumxwnsszso branch from 4013a04 to 7548ca5 Compare April 10, 2026 12:32
@Kha Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Apr 10, 2026
@Kha Kha changed the base branch from nightly-with-mathlib to master April 10, 2026 12:33
@Kha Kha changed the title [REBASED] fix: respect visibility in initialize/builtin_initialize fix: respect visibility in initialize/builtin_initialize Apr 10, 2026
@leanprover-bot leanprover-bot merged commit d53b46a into leanprover:master Apr 10, 2026
25 of 31 checks passed
@Kha Kha mentioned this pull request Apr 10, 2026
Closed
3 tasks
@Kha Kha deleted the push-nmumxwnsszso branch April 10, 2026 13:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

@datokrat datokrat Awaiting requested review from datokrat

@digama0 digama0 Awaiting requested review from digama0

@kim-em kim-em Awaiting requested review from kim-em

@mhuisi mhuisi Awaiting requested review from mhuisi

@tydeu tydeu Awaiting requested review from tydeu

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference 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 merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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

@Kha @leanprover-bot