feat: language reference links and examples in docstrings #7240
Conversation
This file contains 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
Docstrings are now pre-processed as follows: * Output included as part of examples is shown with leading line comment indicators in hovers * URLs of the form `lean-manual://section/section-id` are rewritten to links that point at the corresponding section in the Lean reference manual. The reference manual's base URL is configured when Lean is built and can be overridden with the `LEAN_MANUAL_ROOT` environment variable. This way, releases can point documentation links to the correct snapshot, and users can use their own, e.g. for offline reading. Manual URLs in docstrings are validated when the docstring is added. The presence of a URL starting with `lean-manual://` that is not a syntactically valid section link causes the docstring to be rejected. This allows for future extensibility to the set of allowed links. There is no validation that the linked-to section actually exists. A stage0 update will be required to make the documentation site configurable at build time and for releases.
david-christiansen
added
the
changelog-server
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Feb 26, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Feb 26, 2025
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
src/Lean/DocString/Links.lean
Outdated
| -/ | ||
| def rewriteManualLinks (docString : String) : BaseIO String := do | ||
| let (errs, str) ← rewriteManualLinksCore docString | ||
| assert! errs.isEmpty |
There was a problem hiding this comment.
@mhuisi I wonder whether this line should instead append an error report to the docstring in question. The risk is that this might be missed in cases where docstrings are added via the low-level API by metaprogramming. On the other hand, it may be easier to recover from. I think I'll push a commit that does this, and we can revert it if you disagree.
There was a problem hiding this comment.
Updated in 9de9505. I think it's much better.
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Feb 26, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Feb 26, 2025
|
Please hold off on merges until after the upcoming RC is out. It's too late in the process to add a step to the release process this time around. |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Feb 26, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Feb 26, 2025
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 adds a canonical syntax for linking to sections in the language reference along with formatting of examples in docstrings according to the docstring style guide.
Docstrings are now pre-processed as follows:
Output included as part of examples is shown with leading line comment indicators in hovers
URLs of the form
lean-manual://section/section-idare rewritten to links that point at the corresponding section in the Lean reference manual. The reference manual's base URL is configured when Lean is built and can be overridden with theLEAN_MANUAL_ROOTenvironment variable. This way, releases can point documentation links to the correct snapshot, and users can use their own, e.g. for offline reading.Manual URLs in docstrings are validated when the docstring is added. The presence of a URL starting with
lean-manual://that is not a syntactically valid section link causes the docstring to be rejected. This allows for future extensibility to the set of allowed links. There is no validation that the linked-to section actually exists. To provide the best possible error messages in case of validation failures,Lean.addDocStringnow takes aTSyntax ``docCommentinstead of a string; clients should adapt by removing the step that extracts the string, or by calling the lower-leveladdDocStringCorein cases where the docstring in question is obtained from the environment and has thus already had its links validated.A stage0 update is required to make the documentation site configurable at build time and for releases. A local commit on top of a stage0 update that will be sent in a followup PR includes the configurable reference manual root and updates to the release checklist.