Skip to content

Conversation

@Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Oct 9, 2025

This PR fixes name mangling to be unambiguous / injective by adding 00 for disambiguation where necessary. Additionally, the inverse function, Lean.Name.unmangle has been added which can be used to unmangle a mangled identifier. This unmangler has been added to demonstrate the injectivity but also to allow unmangling identifiers e.g. for debugging purposes.

Closes #10724

@github-actions github-actions bot added the changelog-compiler Compiler, runtime, and FFI label Oct 9, 2025
@Rob23oba Rob23oba marked this pull request as ready for review October 9, 2025 16:35
@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 Oct 9, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 9, 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 f9e140838e5fb12f0726de36bcdf451eb08559fe --onto c32a57e5806476ed6bac4c9cf1bb11cea2b02ea2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-09 18:39:27)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9e140838e5fb12f0726de36bcdf451eb08559fe --onto 705dac4f77aa60d749ee2b37d102518d772d6e53. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-10 14:34:52)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9e140838e5fb12f0726de36bcdf451eb08559fe --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-14 16:23:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9e140838e5fb12f0726de36bcdf451eb08559fe --onto 135e7e7bd3908515354137c952f0d40945fff757. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-20 19:02:42)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9e140838e5fb12f0726de36bcdf451eb08559fe --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-21 12:38:31)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56f3ca6fc74ad5bfbc0feafc4d5a48e87571db62 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-21 20:16:15)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 63c06725bbe73c7316831c35e3e8d7c0e4e9be12 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-22 22:06:10)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 9, 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 f9e140838e5fb12f0726de36bcdf451eb08559fe --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-09 18:39:28)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 56f3ca6fc74ad5bfbc0feafc4d5a48e87571db62 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-21 20:16:17)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 63c06725bbe73c7316831c35e3e8d7c0e4e9be12 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-22 22:06:12)

@Rob23oba Rob23oba requested a review from hargoniX as a code owner October 10, 2025 12:34
@Rob23oba Rob23oba requested a review from kim-em as a code owner October 14, 2025 13:39
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Oct 16, 2025
Copy link
Contributor

@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

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

Great work! Just a few conceptual remarks regarding whether we really want as much proof in here at this point in time.

@hargoniX hargoniX added this pull request to the merge queue Oct 21, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 21, 2025
@hargoniX hargoniX added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Oct 21, 2025
@hargoniX
Copy link
Contributor

This is a bit odd, the change failed to compile in merge queue but works here. @Rob23oba could you rebase on master to see if the issue reproduces in the PR CI?

@Rob23oba
Copy link
Contributor Author

Hmm I hope it's not non-deterministic...

@hargoniX hargoniX added this pull request to the merge queue Oct 23, 2025
Merged via the queue into leanprover:master with commit fad0e69 Oct 23, 2025
17 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
This PR fixes name mangling to be unambiguous / injective by adding `00`
for disambiguation where necessary. Additionally, the inverse function,
`Lean.Name.unmangle` has been added which can be used to unmangle a
mangled identifier. This unmangler has been added to demonstrate the
injectivity but also to allow unmangling identifiers e.g. for debugging
purposes.

Closes leanprover#10724
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Name mangling is not injective

5 participants