Skip to content

chore(*): small docstring syntax fixes#38157

Open
Vierkantor wants to merge 4 commits intoleanprover-community:masterfrom
Vierkantor:fix-docstring-syntax2
Open

chore(*): small docstring syntax fixes#38157
Vierkantor wants to merge 4 commits intoleanprover-community:masterfrom
Vierkantor:fix-docstring-syntax2

Conversation

@Vierkantor
Copy link
Copy Markdown
Contributor

This PR goes through and corrects all the warnings raised by linter.style.docStringVerso that are unrelated to LaTeX or link syntax. In addition to putting backticks around some expressions, there are a few typos (such as mismatched brackets, or syntax in the wrong order), a few unusual usages of punctuation (such as putting {} around names in references), and a few usages made consistent (*-ring, C⋆-algebra).


Open in Gitpod

This PR goes through and corrects all the warnings raised by `linter.style.docStringVerso` that are unrelated to LaTeX or link syntax. In addition to putting backticks around some expressions, there are a few typos (such as mismatched brackets, or syntax in the wrong order), a few unusual usages of punctuation (such as putting `{}` around names in references), and a few usages made consistent (`*`-ring, C⋆-algebra).
@Vierkantor Vierkantor added documentation Improvements or additions to documentation tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels Apr 17, 2026
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 17, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 20, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 20, 2026

PR summary 4fceb4697e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Comment thread Mathlib/Algebra/Category/Grp/AB.lean Outdated
Comment thread Mathlib/Algebra/Category/ModuleCat/AB.lean Outdated
Comment thread Mathlib/Algebra/Star/CentroidHom.lean Outdated
When a (nonunital, non-associative) semiring is equipped with an involutive automorphism the
center of the centroid becomes a star ring in a natural way and the natural mapping of the centre of
the semiring into the centre of the centroid becomes a *-homomorphism.
the semiring into the centre of the centroid becomes a `*`-homomorphism.
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Just as with the AB axioms... What is the correct way to write an asterisk in markdown / verso? Does escaping work?

Suggested change
the semiring into the centre of the centroid becomes a `*`-homomorphism.
the semiring into the centre of the centroid becomes a \*-homomorphism.

Idem dito for many other places.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

According to grep, we have about twice as many `*`-objects (39) in docstrings compared to *-objects (22). But indeed we could switch over to \*-objects, since both Markdown (CommonMark) and Verso allow backslash-escaping *.

Some more datapoints: looks like Wikipedia writes them as *-objects and the nLab writes them as $*$-objects.

I suppose \*-objects render the most naturally, so let's go for that.

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 20, 2026
@Vierkantor Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 20, 2026
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 20, 2026

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 20, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). documentation Improvements or additions to documentation tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants