feat: docstrings with Verso syntax#10307
Merged
david-christiansen merged 25 commits intoleanprover:masterfrom Sep 10, 2025
Merged
feat: docstrings with Verso syntax#10307david-christiansen merged 25 commits intoleanprover:masterfrom
david-christiansen merged 25 commits intoleanprover:masterfrom
Conversation
This makes it run at the right time and makes it consistent with the rest of the system.
Comment on lines
+11
to
+34
| attribute [doc_role] Lean.Doc.name | ||
| attribute [doc_role] Lean.Doc.kw | ||
| attribute [doc_role] Lean.Doc.kw? | ||
| attribute [doc_role] Lean.Doc.syntaxCat | ||
| attribute [doc_role] Lean.Doc.option | ||
| attribute [doc_role] Lean.Doc.attr | ||
| attribute [doc_role] Lean.Doc.tactic | ||
| attribute [doc_role] Lean.Doc.conv | ||
| attribute [doc_code_block] Lean.Doc.lean | ||
| attribute [doc_code_block] Lean.Doc.output | ||
| attribute [doc_command] Lean.Doc.«open» | ||
| attribute [doc_command] Lean.Doc.«set_option» | ||
| attribute [doc_role] Lean.Doc.given | ||
| attribute [doc_role lean] Lean.Doc.leanTerm | ||
| attribute [doc_role] Lean.Doc.manual | ||
| attribute [doc_role] Lean.Doc.syntax | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestName | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestLean | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestTactic | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestAttr | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestOption | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestKw | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestCat | ||
| attribute [doc_code_suggestions] Lean.Doc.suggestSyntax |
Contributor
Author
There was a problem hiding this comment.
These lines will be deleted after the stage0 update.
| add := fun decl stx _ => do | ||
| Attribute.Builtin.ensureNoArgs stx | ||
| declareBuiltinDocStringAndRanges decl | ||
| applicationTime := AttributeApplicationTime.afterCompilation |
Contributor
Author
There was a problem hiding this comment.
afterCompilation attributes are applied after documentation is added, so this is necessary here so the docs will be present.
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
kim-em
added a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 11, 2025
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 11, 2025
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 11, 2025
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 15, 2025
* fix deprecations * remove upstreamed defs * two fixes * fix merge * fix merge * revert sqrt changes * ugh * fix from nightly-testing * fix merge * remove test deleted on master * fix test * note about test * . * Update lean-toolchain for leanprover/lean4#10194 * chore: bump to nightly-2025-09-02 * adjust to upstream changes * fix * fix * long line * Use Mathlib's nightly toolchain to run docgen in the nightly test * simpNF linter * whitespace * Update lean-toolchain for testing leanprover/lean4#10217 * Correct the working directory: should be 'docbuild' * Rework the grind regression report as a nightly-testing regression report It should still report the same things, but now as one message for all regression kinds * feat(Cache): download speeds & more info on errors * fix(Cache): add base download failure message * fixes * turn off linter * adaptation note * turn off linter.nightlyRegressionSet * chore: adaptations for nightly-2025-09-02 * Update lean-toolchain for testing leanprover/lean4#10059 * Update lean-toolchain for leanprover/lean4#10217 * chore: bump to nightly-2025-09-03 * Remove the erroring nightly regression report, we'll develop this on another branch. * fixes * update LibraryRewrite test * Update lean-toolchain for leanprover/lean4#10059 * chore: bump to nightly-2025-09-04 * fix * chore: bump to nightly-2025-09-05 * chore: adaptations for nightly-2025-09-05 * chore: bump to nightly-2025-09-06 * Update lean-toolchain for testing leanprover/lean4#10271 * Adapt to leanprover/lean4#10271 * Bump batteries * Update lean-toolchain for leanprover/lean4#10271 * chore: bump to nightly-2025-09-07 * nolint unusedArguments * Merge master into nightly-testing * chore: bump to nightly-2025-09-08 * fixes * chore: bump to nightly-2025-09-09 * fix thing * Update lean-toolchain for testing leanprover/lean4#10306 * temporarily remove test * adaptation note * master version of Cache/Requests.lean * chore: bump to nightly-2025-09-10 * adaptation note * chore: adaptations for nightly-2025-09-10 * merge lean-pr-testing-10059 * bump toolchain manually?? * restore test * chore: bump to nightly-2025-09-11 * lake update * fix * adaptations for leanprover/lean4#10307 * remove validateDocComment in ToAdditive * remove upstreamed Function.Injective * update assert_not_exists * oops * comment out DeriveTraversable * chore: replace some grind attibutes with grind_pattern, to be robust for future heuristic changes * suggestions from Rob23oba * lshake --fix * fix bad shake * shake --update * . * chore: adaptations for nightly-2025-09-11 * chore: bump to nightly-2025-09-12 * Revert "oops" This reverts commit 517b832. * Revert "comment out DeriveTraversable" This reverts commit 0460eb8. * fix DeriveTraversable * add `binders` fields * fix * fixes * update manifest * fixes * fixes * fixes * chore: bump to nightly-2025-09-13 * fixes * fixes * fixes * fixes * fixes * fixes * fixes * remove adaptation note * Update lean-toolchain for testing leanprover/lean4#10373 * fixes * chore: bump to nightly-2025-09-14 * Update lean-toolchain for testing leanprover/lean4#10377 * fix * fix * fix * fix emrge * update batteries * chore: adaptations for nightly-2025-09-14 * Merge master into nightly-testing * Update Mathlib/Data/List/Basic.lean * Merge master into nightly-testing * chore: adaptations for nightly-2025-09-14 * chore: bump to nightly-2025-09-15 --------- Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
david-christiansen
added a commit
to david-christiansen/lean4
that referenced
this pull request
Oct 10, 2025
This PR fixes a regression introduced by leanprover#10307, where hovering the name of an inductive type or constructor in its own declaration didn't show the docstring. In the process, a bug in docstring handling for coinductive types was discovered and also fixed. Tests are added to prevent the regression from repeating in the future.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Oct 15, 2025
This PR fixes a regression introduced by #10307, where hovering the name of an inductive type or constructor in its own declaration didn't show the docstring. In the process, a bug in docstring handling for coinductive types was discovered and also fixed. Tests are added to prevent the regression from repeating in the future.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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 upstreams the Verso parser and adds preliminary support for Verso in docstrings. This will allow the compiler to check examples and cross-references in documentation.
After a
stage0update, a follow-up PR will add the appropriate attributes that allow the feature to be used. The parser tests from Verso also remain to be upstreamed, and user-facing documentation will be added once the feature has been used on more internals.