Skip to content

Conversation

@grunweg
Copy link
Collaborator

@grunweg grunweg commented Nov 19, 2025

Mostly as a learning exercise for me to understand the module system better.


Open in Gitpod

@grunweg grunweg added the awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. label Nov 19, 2025
@github-actions github-actions bot added the t-linter Linter label Nov 19, 2025
@github-actions
Copy link

github-actions bot commented Nov 19, 2025

PR summary 082440f5b2

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- ErrorFormat
- Lean.Name.isLocal
- copyrightHeaderChecks
- deprecatedNoSince
- directoryDependencyCheck
- extractOpenNames
- findImports
- getDeclModifiers
- getImportIds
- isCDot?
- isSetOption
- mkWindow
- structureInType

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

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

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


No changes to technical debt.

You can run this locally as

./scripts/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).

/-- Verifies that all modules in `modules` are named in `UpperCamelCase`
(except for explicitly discussed exceptions, which are hard-coded here).
Return the number of modules violating this. -/
public -- only for MathlibTest/ModuleCase.lean
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

One might argue that this is useful public API (as evidenced by the unit tests). If so, I'll be happy to remove the comment.

Source: https://learn.microsoft.com/en-gb/windows/win32/fileio/naming-a-file.
Return the number of module names violating this rule. -/
public -- only for `MathlibTest/ForbiddenModuleNames`
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

As above

@grunweg grunweg changed the title chore(Tactic/Linters): remove most public section chore(Tactic/Linters): remove public section Nov 19, 2025
@github-actions github-actions bot removed the awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. label Nov 19, 2025
@grunweg
Copy link
Collaborator Author

grunweg commented Nov 19, 2025

!bench

@grunweg
Copy link
Collaborator Author

grunweg commented Nov 19, 2025

(Just in case, I would be a bit surprised to see any effect.)

@leanprover-radar
Copy link

leanprover-radar commented Nov 19, 2025

Benchmark results for 97e228b against 6a54a80 are in! @grunweg

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 97e228b.
There were no significant changes against commit 6a54a80.

@github-actions
Copy link

File Instructions %
build +287.39⬝10⁹ (+0.16%)
lint -1.43⬝10⁹ (-0.01%)
2 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Preadditive.Biproducts +1.183⬝10⁹ (+1.75%)
Mathlib.Tactic.CC.Lemmas +1.117⬝10⁹ (+33.70%)

CI run Lakeprof report

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 20, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 20, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-linter Linter

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants