[Merged by Bors] - feat: a linter to deprecate imported modules by adomani · Pull Request #20987 · leanprover-community/mathlib4

adomani · 2025-01-23T13:34:28Z

Writing

import Bar1
import Bar2

deprecated_module (since := "yyyy-mm-dd")

in file A.lean means that any file that imports A will have import A flagged with a suggestion to import Bar1 and Bar2 instead.

Zulip discussion

github-actions · 2025-01-23T13:35:36Z

PR summary 988edcd197

Import changes exceeding 2%

%	File
+6.25%	`Mathlib.Tactic.Linter`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter	32	34	+2 (+6.25%)
Mathlib.Tactic	2686	2688	+2 (+0.07%)

Import changes for all files

Files	Import difference
There are 5363 files with changed transitive imports taking up over 231742 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

+ addModuleDeprecation
+ deprecated.moduleLinter

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

eric-wieser · 2025-01-23T13:50:14Z

Maybe deprecate_module would be a better name?

Mathlib/Tactic/Linter/DeprecateModules.lean

adomani · 2025-01-23T17:07:52Z

!bench

adomani · 2025-01-23T17:09:14Z

!bench

grunweg

I don't have strong opinions on the environment extension set-up (for lack for time spent with them); the remaining infrastructure looks very good. Find below my usual collection of small polish comments.

Mathlib/Tactic/Linter/DeprecateModule.lean

grunweg · 2025-01-23T17:13:55Z

Mathlib/Tactic/Linter/DeprecateModule.lean

+elab "show_deprecated_modules" : command => do
+  let directImports := deprecateModuleExt.getState (← getEnv)
+  logInfo <| "\n".intercalate <|
+    directImports.fold (init := ["Deprecated modules\n"]) fun nms (i, deps) =>


I'm pretty sure there's room for bikeshedding this formatting. I think we can land something and iterate.

Can we use the same import linking that find_home emits?

I don't have time to look into this now, but I like the idea!

Mathlib/Tactic/Linter/DeprecateModule.lean

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

…over-community/mathlib4 into adomani/deprecated_imports_linter

leanprover-bot · 2025-01-23T17:59:22Z

Here are the benchmark results for commit c2b50b2.
There were no significant changes against commit 8fac96b.

github-actions · 2025-01-23T17:59:44Z

File	Instructions	%
`build`	+327.990⬝10⁹	(+0.21%)
`Mathlib.RingTheory.Kaehler.JacobiZariski`	+1.42⬝10⁹	(+0.12%)
CI run

adomani

Thanks, Michael!

I acted on all comments, except extracting the code from the header linter, since that would take a little more thought.

Mathlib/Tactic/Linter/DeprecateModule.lean

adomani · 2025-01-23T19:49:36Z

!bench

leanprover-bot · 2025-01-23T20:18:38Z

Here are the benchmark results for commit 5191403.
There were no significant changes against commit 8fac96b.

github-actions · 2025-01-23T20:19:01Z

File	Instructions	%
`build`	+208.707⬝10⁹	(+0.13%)
`Mathlib.Data.Array.Lemmas`	+1.495⬝10⁹	(+50.67%)
CI run

Mathlib/Tactic/Linter/DeprecateModule.lean

adomani · 2025-04-12T13:34:57Z

We now have MathlibTest/{DeprecatedModule,DeprecatedModuleTest1,DeprecatedModuleTest2} - I wouldn't mind to the first two files being merged either. That's not something I'd insist on, though.

I removed the intermediate MathlibTest/DeprecatedModuleTest1, leaving only MathlibTest/DeprecatedModule and MathlibTest/DeprecatedModuleTest.

grunweg · 2025-04-12T20:26:23Z

I don't have an opinion on whether importing it early or not. An alternative could be that the linter, by default, does not suggest itself as an import.

The latter option sounds good. I could implement that tweak tomorrow (or so).

adomani · 2025-04-12T20:59:22Z

I don't have an opinion on whether importing it early or not. An alternative could be that the linter, by default, does not suggest itself as an import.

The latter option sounds good. I could implement that tweak tomorrow (or so).

This modification was easy enough that I just pushed it.

grunweg · 2025-04-12T21:37:46Z

(The current state still looks good to me.)

Mathlib/Tactic/Linter/DeprecatedModule.lean

kim-em · 2025-04-12T22:48:15Z

Optional, but it might be nice to allow an optional text argument, that would be displayed with the suggestion.

kim-em · 2025-04-12T22:48:53Z

bors d+

mathlib-bors · 2025-04-12T22:48:56Z

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

adomani · 2025-04-13T06:15:34Z

Kim, thank you for the suggestions!

@grunweg I implemented all of Kim's changes: if you want to take a look at them, I'll wait for a few hours before merging.

grunweg · 2025-04-13T07:19:28Z

The changes look great to me; I just pushed one more test.

grunweg · 2025-04-13T07:20:08Z

I'm not sure how to fix the CI failure. The error is unable to locate share/zoneinfo in the local timezone database at '/etc/localtime'; presumably, something needs to be installed on the test runners.

…imports_linter

adomani · 2025-04-13T17:55:19Z

I commented out the failing test: it was failing due to some incompatibility of the date package with the CI settings, so it was not really something prejudicial for the PR.

Assuming that this version passes CI, I will merge and we can see whether we want to fix the CI setup in a separate PR.

adomani · 2025-04-13T18:41:19Z

bors merge

Writing ```lean import Bar1 import Bar2 deprecated_module since yyyy-mm-dd ``` in file `A.lean` means that any file that imports `A` will have `import A` flagged with a suggestion to import `Bar1` and `Bar2` instead. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Deprecated.60.20folder) Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-04-13T18:48:01Z

Pull request successfully merged into master.

Build succeeded:

Writing ```lean import Bar1 import Bar2 deprecated_module since yyyy-mm-dd ``` in file `A.lean` means that any file that imports `A` will have `import A` flagged with a suggestion to import `Bar1` and `Bar2` instead. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Deprecated.60.20folder) Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

feat: a linter to deprecate imported modules

3eed855

github-actions bot added the t-linter Linter label Jan 23, 2025

rename to deprecate_modules, import in Linter

025148c

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 23, 2025

eric-wieser reviewed Jan 23, 2025

View reviewed changes

Mathlib/Tactic/Linter/DeprecateModules.lean Outdated Show resolved Hide resolved

adomani added 2 commits January 23, 2025 16:30

more consistent use of deprecate_module

c2b50b2

whitespace

d4ac603

grunweg reviewed Jan 23, 2025

View reviewed changes

grunweg mentioned this pull request Jan 23, 2025

[Merged by Bors] - chore: deprecate the file AnalyticManifold #20979

Closed

1 task

adomani and others added 3 commits January 23, 2025 17:55

Michael's comments

5a83fce

Apply suggestions from code review

9ff5346

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

Merge branch 'adomani/deprecated_imports_linter' of github.com:leanpr…

dfae533

…over-community/mathlib4 into adomani/deprecated_imports_linter

adomani commented Jan 23, 2025

View reviewed changes

adomani added 3 commits January 23, 2025 18:00

typo

3cc0a34

loop also through repetitions

a7db3c3

test earlier

5191403

eric-wieser reviewed Jan 23, 2025

View reviewed changes

Mathlib/Tactic/Linter/DeprecateModule.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 23, 2025

View reviewed changes

Mathlib/Tactic/Linter/DeprecateModule.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 23, 2025

View reviewed changes

Mathlib/Tactic/Linter/DeprecateModule.lean Outdated Show resolved Hide resolved

adomani added 2 commits January 24, 2025 12:15

rename with d

5a9685b

nest option name

8b78d24

adomani added 2 commits April 12, 2025 15:32

use DeprecatedModule in test

3e97025

reduce one file

ae1a8e4

do not suggest importing Mathlib.Tactic.Linter.DeprecatedModule

6a79de9

kim-em reviewed Apr 12, 2025

View reviewed changes

Mathlib/Tactic/Linter/DeprecatedModule.lean Outdated Show resolved Hide resolved

kim-em reviewed Apr 12, 2025

View reviewed changes

Mathlib/Tactic/Linter/DeprecatedModule.lean Outdated Show resolved Hide resolved

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 12, 2025

Add date parsing, optional string, align since syntax

3764645

One more test

2c473ce

adomani added 2 commits April 13, 2025 19:47

Merge remote-tracking branch 'origin/master' into adomani/deprecated_…

fbda482

…imports_linter

comment out test

988edcd

ghost added the ready-to-merge This PR has been sent to bors. label Apr 13, 2025

mathlib-bors bot changed the title ~~feat: a linter to deprecate imported modules~~ [Merged by Bors] - feat: a linter to deprecate imported modules Apr 13, 2025

mathlib-bors bot closed this Apr 13, 2025

mathlib-bors bot deleted the adomani/deprecated_imports_linter branch April 13, 2025 18:48

Conversation

adomani commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 988edcd197

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Jan 23, 2025

Uh oh!

Uh oh!

adomani commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

adomani commented Jan 23, 2025

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg Jan 23, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jan 23, 2025

Choose a reason for hiding this comment

Uh oh!

adomani Jan 24, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leanprover-bot commented Jan 23, 2025

Uh oh!

github-actions bot commented Jan 23, 2025

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adomani commented Jan 23, 2025

Uh oh!

leanprover-bot commented Jan 23, 2025

Uh oh!

github-actions bot commented Jan 23, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adomani commented Apr 12, 2025

Uh oh!

grunweg commented Apr 12, 2025

Uh oh!

adomani commented Apr 12, 2025

Uh oh!

grunweg commented Apr 12, 2025

Uh oh!

Uh oh!

Uh oh!

kim-em commented Apr 12, 2025

Uh oh!

kim-em commented Apr 12, 2025

Uh oh!

mathlib-bors bot commented Apr 12, 2025

Uh oh!

adomani commented Apr 13, 2025

adomani commented Jan 23, 2025 •

edited

Loading

github-actions bot commented Jan 23, 2025 •

edited

Loading

adomani commented Jan 23, 2025 •

edited

Loading