fix: encode spaces in library_note declaration names for export format compatibility #1601
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
awaiting-review
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jan 6, 2026
kim-em
force-pushed
the
fix-library-note-export-format
branch
2 times, most recently
from
51a04d6 to
beba113
Compare
…t compatibility The Lean export format (used by `lean4export` and consumed by external type checkers like `nanoda_lib`) does not support whitespace in declaration names. Since PR #1545, `library_note` creates actual declarations like `LibraryNote.«my note»`, which contain literal spaces and cannot be exported. This PR encodes spaces as underscores in declaration names while preserving the original name (with spaces) in the environment extension for `#help note` lookup. For example, `library_note «my library note»` now creates a declaration named `LibraryNote.my_library_note` instead of `LibraryNote.«my library note»`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
kim-em
force-pushed
the
fix-library-note-export-format
branch
from
beba113 to
878f333
Compare
Collaborator
|
Mathlib CI status (docs):
|
Collaborator
|
Looks fine to me. Note that this isn't a solution to the underlying issue since Lean does allow identifiers with spaces. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR fixes a compatibility issue between
library_noteand the Lean export format.The Problem
Since PR #1545 (merged Dec 9, 2025),
library_notecreates actual declarations in theLibraryNotenamespace. When library notes have human-readable names with spaces like«norm_num lemma function equality», this creates declarations like:The current Lean export format (used by
lean4exportand consumed by external type checkers like nanoda_lib) does not support whitespace in declaration names. This means Mathlib cannot be exported and verified by external type checkers.See discussion:
The Fix
This PR encodes spaces as underscores in declaration names while preserving the original name (with spaces) in the environment extension for
#help notelookup.For example:
library_note «my library note»now createsLibraryNote.my_library_note#help note "my"still finds and displays the note correctlyWhy This Matters
This fix is essential for enabling external verification of Mathlib. Without it:
lean4exportcannot export Mathlibnanoda_lib(an independent Lean 4 type checker in Rust) cannot verify MathlibThe export format may be generalized to JSON in the future (see the GitHub issue above), but this fix provides immediate compatibility with the current format.
🤖 Prepared with Claude Code