Skip to content

[Merged by Bors] - chore(Geometry/Manifold): make some doc-strings follow the style guide#39729

Closed
grunweg wants to merge 5 commits into
leanprover-community:masterfrom
grunweg:diffgeo-docstrings-preelaborators
Closed

[Merged by Bors] - chore(Geometry/Manifold): make some doc-strings follow the style guide#39729
grunweg wants to merge 5 commits into
leanprover-community:masterfrom
grunweg:diffgeo-docstrings-preelaborators

Conversation

@grunweg

@grunweg grunweg commented May 22, 2026

Copy link
Copy Markdown
Contributor

such as, by them beginning with the object they are defining as a subject.
This will yield much better doc-strings for the differential geometry elaborators in #39677.

It also increases conformance with the documentation style guide.

Inspired by the MI retreat in Lisbon.


Open in Gitpod

@grunweg
grunweg force-pushed the diffgeo-docstrings-preelaborators branch from b224b9b to 8cf19e5 Compare May 22, 2026 23:52
@github-actions github-actions Bot added the t-differential-geometry Manifolds etc label May 22, 2026
@github-actions

github-actions Bot commented May 22, 2026

Copy link
Copy Markdown

PR summary 106ab480a9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

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

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

Lean-aware diff — post-build, computed from the Lean environment (commit 106ab48).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit 106ab480a9
Reference commit 8d1ee6c7d5

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

@grunweg

grunweg commented May 22, 2026

Copy link
Copy Markdown
Contributor Author

@Vierkantor on the stylistic aspect (only if you'd like)

@grunweg
grunweg force-pushed the diffgeo-docstrings-preelaborators branch from 8cf19e5 to 9dcaa53 Compare May 26, 2026 22:10
@ocfnash ocfnash removed their assignment May 28, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts 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 May 31, 2026
@mathlib-merge-conflicts

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@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 May 31, 2026
@grunweg
grunweg force-pushed the diffgeo-docstrings-preelaborators branch from abb35a6 to c2d5d9a Compare May 31, 2026 15:44
@PatrickMassot

Copy link
Copy Markdown
Member

bors merge

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 22, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jun 22, 2026
#39729)

such as, by them beginning with the object they are defining as a subject.
This will yield much better doc-strings for the differential geometry elaborators in #39677.

It also increases conformance with the [documentation style guide](https://github.com/leanprover/lean4/blob/master/doc/style.md).

Inspired by the MI retreat in Lisbon.
@mathlib-bors

mathlib-bors Bot commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(Geometry/Manifold): make some doc-strings follow the style guide [Merged by Bors] - chore(Geometry/Manifold): make some doc-strings follow the style guide Jun 22, 2026
@mathlib-bors mathlib-bors Bot closed this Jun 22, 2026
@grunweg
grunweg deleted the diffgeo-docstrings-preelaborators branch June 22, 2026 10:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants