Skip to content

feat(Tactic/Linter/ValidatePRTitle): do not check the capitalisation of the commit subject - #43136

Open
joneugster wants to merge 2 commits into
leanprover-community:masterfrom
joneugster:feat/disable-commit-linter-capitalisation
Open

feat(Tactic/Linter/ValidatePRTitle): do not check the capitalisation of the commit subject#43136
joneugster wants to merge 2 commits into
leanprover-community:masterfrom
joneugster:feat/disable-commit-linter-capitalisation

Conversation

@joneugster

Copy link
Copy Markdown
Contributor

There have been false-positives on abbreviations and proper names which seem to justify not to lint for this.


#mathlib reviewers > Check PR title

Open in Gitpod

@joneugster joneugster added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 26, 2026
@github-actions github-actions Bot added the t-linter Linter label Aug 26, 2026
@github-actions

github-actions Bot commented Aug 26, 2026

Copy link
Copy Markdown

PR summary fe7618ebc9

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 fe7618e).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.


No changes to strong technical debt.
No changes to weak technical debt.

Current commit fe7618ebc9
Reference commit 5ce203ecd5

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.py 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).

@mathlib-dependent-issues

Copy link
Copy Markdown

@joneugster joneugster added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Aug 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-linter Linter

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant