deprecated_module

Stream: general

[Andrew Yang]

What is the policy on deprecated modules? Are they required and must they be done in the same PR? The down side of it being in the same PR is that it botches the diff (and by extension the git history but I am willing to give this up) and make trivial PRs moving files significantly harder to review. I heard there are discussions about having a bot do this automatically after the moving PR is merged but are we anywhere near this?

[Michael Rothgang]

The status is: the file-removed label is now managed well, and this is waiting for somebody to implement the final bot. I sketched some implementation instructions in the third bullet here, but won't have too much time to implement it. Help is welcome!

[Michael Rothgang]

Another option is to simply create the follow-up by hand and ping in this channel for review. I'm happy to maintainer merge such PRs quickly --- but presumably the "speedy review" channel could also work just fine.

[Christian Merten]

Andrew Yang said:

What is the policy on deprecated modules? Are they required and must they be done in the same PR? The down side of it being in the same PR is that it botches the diff (and by extension the git history but I am willing to give this up) and make trivial PRs moving files significantly harder to review. I heard there are discussions about having a bot do this automatically after the moving PR is merged but are we anywhere near this?

I recently (in #24788) put a link to the diff before the module deprecation commit below the PR description. That way this diff is easy to review and there is not the annoying overhead of an immediate follow-up PR.

[Eric Wieser]

I've just seen a strong reason to do this in a separate PR; if you don't the conflicts downstream are not automatically resolved

[Eric Wieser]

That is, all of the following are reasons to care about the history:

• Review (solved with helpful comments)
• Blame (rare-ish use-case)
• Syncing PRs to HEAD (hard to fix without just creating the right history to start with)

[Damiano Testa]

How about this.

On every commit to master,

• find the files in Mathlib/ that have been removed,
• regenerate them up to their final import,
• append the deprecated_module command,
• create a branch with this and
• ping this channel about it?

Have I missed something?

[Michael Rothgang]

(You could refine this by only running the workflow if a PR with the file-removed label was merged. I'm not sure how easy or difficult that is.)

[Michael Rothgang]

I'd add "or moved" to the first bullet ---- otherwise, looks spot on!

[Damiano Testa]

Well, I was thinking of not using gits interface for the removed files, but actually bash-diff'ing the .lean files. That should catch renames, as it won't be aware of the files' contents.

[Damiano Testa]

Which makes me wonder: does git index empty files?

[Damiano Testa]

Are empty files allowed in mathlib?

[Damiano Testa]

(I suspect that both answers are yes and that I'd rather the second at least be no.)

[Michael Rothgang]

Quick searching suggests that empty files are allowed (of course they are). And I don't see any mechanism to forbid empty files in mathlib. We could add one, though.

[Michael Rothgang]

For lean files, the mk_all step ensures all files are present. (It doesn't check emptiness, though. I could add that to the lint-style linter, though.)

[Kevin Buzzard]

Empty files in FLT don't lint, because they're missing an import. Does this help?

[Michael Rothgang]

... and this is because otherwise the flexible linter is not recognised. Right. But mathlib doesn't enable that linter (yet?).

[Damiano Testa]

My main concern is that there is therefore a difference between removing a file and simply emptying it. The module deprecation script can also take care of handling empty files, but I suspect that doing this elsewhere is better.

[Damiano Testa]

By the way, I almost have a script ready.

[Michael Rothgang]

I agree with both your points: handling empty files (e.g. by disallowing them) would be good, and should happen elsewhere.

[Damiano Testa]

Ok, I'll write the script assuming that there are no empty files.

[Damiano Testa]

#24861 introduces the #create_deprecated_modules command.

[Damiano Testa]

From the doc-string:

The command #create_deprecated_modules (n)? (comment)? (write)? generates deprecated modules.

Writing

#create_deprecated_modules 5 "These files are no longer relevant"

looks at the lean files in Mathlib that existed 4 commits ago
(i.e. the commit that you see with git log -5) and that are no longer present.
It shows how the corresponding deprecated modules should look like, using
"These files are no longer relevant" as the (optional) comment.

If the number of commits is not explicitly used, #create_deprecated_modules defaults to 2,
namely, the commit just prior to the current one.

If the message is not explicitly used, #create_deprecated_modules defaults to
"Auto-generated deprecation".
If you wish there to be no comment, use #create_deprecated_modules 5 "".

Note that the command applies the same comment to all the files that it generates.

Finally, if everything looks correct, adding a final write actually generates the files:

#create_deprecated_modules 5 "These files are no longer relevant" write

[Damiano Testa]

I did not integrate it in CI, since there are some potential issues with the same deprecated file being generated multiple times, if the deprecation PRs don't get merged fast enough (and I would rather test that everything is behaving as expected!).

[Michael Rothgang]

Here's a thought on the next step: add a workflow running daily (say, at 11pm --- this will get some deprecations wrong by a day, which may still be fine). Ask git for the number of commits merged that day, and then generate deprecations with that. (Actually, even running it with "100" hard-coded is unlikely do do much harm, if we make sure to only merge the first such PR/double-check the dates.)

[Michael Rothgang]

A first test looks great (and produced #24871)

[Damiano Testa]

Michael, your test shows that the PRs should also run lake exe mk_all before pushing! :lol:

[Michael Rothgang]

Yes!

[Michael Rothgang]

Another procrastination avenue: bisect the commits to find when a particular file was removed, and automatically determine the offending PR and day. (I would say that's not worth it.)

[Michael Rothgang]

Other observation: the script works really well locally. If I commit the generated deprecation, it's "self-silencing" (an exception won't appear), so you can very well bisect manually "which were recent deprecations" and add them one by one. And the script is very fast, so this is pleasant to work with.

[Damiano Testa]

I'm glad that you are finding the script easy to use and workable!

[Damiano Testa]

I think that naming a file to deprecate is a very reasonable extension, as git's --follow should give you quick access to all the information that you need.

[Damiano Testa]

This would be for a later PR, though!

[Damiano Testa]

Btw, were you testing this on Linux?

[Damiano Testa]

(The script is written in Lean, but uses git internally.)

[Michael Rothgang]

Yes, I used Linux (Debian stable).

[Damiano Testa]

Michael, thank you for sharing your workflow in your PR! This is incredible useful! Here are some comments.

1. It would be good if the command ignored filename changes that only differ in upper/lowercase, since those are probably not going to be implemented.
2. More generally, allowing a list of files that are not going to be deprecated is also reasonable, since there will always be exceptions.
3. The command could show the commit message of the past commit that it is using.

[Michael Rothgang]

I definitely agree with 1 and 3. I'm not sure about 2, but won't mind it either.

[Damiano Testa]

Since I expect this command to be eventually used by bots, maybe a simple solution would be to allow the syntax

#create_deprecated_modules 5 "These files are no longer relevant" only <names of modules> write

to let the script know that you only want to deprecate the explicitly given list of modules (and the only ... is optional, kind of a "I'm feeling lucky" option).

[Damiano Testa]

4. Make the command emit a warning when the generated text exceeds 100 characters.

We could even consider silencing the longLine linter on deprecated module messages, since those files may as well never be opened anyway.

[Michael Rothgang]

#24917 is a different version of the same PR: I like the UX a lot (but there seems to be a small bug making it not work on my side)

[Damiano Testa]

I should have fixed the issue: please, let me know if you still experience problems with the command!

[Riccardo Brasca]

The current policy to move a file is to just move it in a PR and create the deprecated module blah blah in another one, right? (This discussion should be public anyway)

[Notification Bot]

This topic was moved here from #mathlib reviewers > deprecated_module by Riccardo Brasca.

[Riccardo Brasca]

I've moved this discussion to #**general> since it is relevant for everybody.

[Riccardo Brasca]

@Xavier Roblot this the discussion I mentioned in #25388

[Kevin Buzzard]

Damiano's "ping this channel" comment now should say "ping a private channel (that not everybody can ping)"

[Bolton Bailey]

Riccardo Brasca said:

The current policy to move a file is to just move it in a PR and create the deprecated module blah blah in another one, right? (This discussion should be public anyway)

I just got told to do this, but I am confused. If I put the deprecated modules in another PR, doesn't that just mean there will be a period where the modules don't have a deprecation warning? What if someoneone makes a dependency on mathlib in the interim?

[Bolton Bailey]

Andrew Yang said:

What is the policy on deprecated modules? Are they required and must they be done in the same PR? The down side of it being in the same PR is that it botches the diff (and by extension the git history but I am willing to give this up) and make trivial PRs moving files significantly harder to review. I heard there are discussions about having a bot do this automatically after the moving PR is merged but are we anywhere near this?

What do you mean when you say it "botches the diff"? Whether you do it over one PR or two, isn't it the same total amount of lines of diff either way?

[Ruben Van de Velde]

Bolton Bailey said:

Riccardo Brasca said:

The current policy to move a file is to just move it in a PR and create the deprecated module blah blah in another one, right? (This discussion should be public anyway)

I just got told to do this, but I am confused. If I put the deprecated modules in another PR, doesn't that just mean there will be a period where the modules don't have a deprecation warning? What if someoneone makes a dependency on mathlib in the interim?

Yes, but it's assumed most people won't update their mathlib right inside the gap

[Ruben Van de Velde]

Bolton Bailey said:

Andrew Yang said:

What is the policy on deprecated modules? Are they required and must they be done in the same PR? The down side of it being in the same PR is that it botches the diff (and by extension the git history but I am willing to give this up) and make trivial PRs moving files significantly harder to review. I heard there are discussions about having a bot do this automatically after the moving PR is merged but are we anywhere near this?

What do you mean when you say it "botches the diff"? Whether you do it over one PR or two, isn't it the same total amount of lines of diff either way?

Git can only detect the change as a move if you don't add a new file at the same path in the same commit

[Bolton Bailey]

Ah, ok, that actually makes sense, thanks for the explanation.

[Ruben Van de Velde]

It's somewhat hacky for sure

[Ruben Van de Velde]

Did we end up automating this? We're missing one for Mathlib/Analysis/SpecialFunctions/Integrals.lean (#26135)

[Michael Rothgang]

The current state of the art is #24917 (which is primarily waiting on completing a review). So, in order:

• finish reviewing #24917 (I reviewed the first 250 lines in detail, another 100 remaining)
• land #24917
• use that to backfill missing deprecations (this could already be done now, using the current state of the branch)
• create a new PR, with automation to periodically search for missing deprecations, create them and making a PR adding them (this is very similar to the nolint workflow)

[Michael Rothgang]

Feel free to make a PR for the missing deprecations! That would be very welcome.

[Michael Rothgang]

(Help with reviewing the infrastructure also is. I do mean to return to this, but my mathlib infra time is short right now, and #26109 feels higher priority.)

[Ruben Van de Velde]

I'm disappointed to discover while bumping sphere-eversion that Mathlib.Analysis.InnerProductSpace.Projection was removed and we didn't add a deprecation in time. If we're not working on automation to prevent this, can we revert to requiring deprecations in the PR that removes the file? I don't think the version history downsides weigh up to the downstream pain if we don't manage to follow up

[Yaël Dillies]

The version history mess really downsides the downstream pain in my opinion

[Ruben Van de Velde]

Then we should find a way to make sure the follow up happens

[Kim Morrison]

Ideally a bot does this, say every night?

[Ruben Van de Velde]

For example, yeah

[Michael Rothgang]

For the record: I finished reviewing #24917 a week ago. Most of it is easy to fix, but there is one bug. Help with tracking that down is certainly welcome.

[Jireh Loreaux]

That's my bad about the projection file. I forgot to remind to follow up with that.

[Ruben Van de Velde]

Fwiw, I ran into another one today, but I forgot to write down which one

[Damiano Testa]

According to one of the commands in the script, in the last 600 commits, these are the missing deprecations:

'Mathlib/Algebra/Group/FiniteSupport.lean' was renamed to
'Mathlib/Algebra/Notation/FiniteSupport.lean' (R089),
but the similarity 89% is less than the expected threshold of 100%.
          We treat this file as a removal.

'Mathlib/Algebra/Notation/Pi.lean' was renamed to
'Mathlib/Algebra/Notation/Pi/Defs.lean' (R080),
but the similarity 80% is less than the expected threshold of 100%.
          We treat this file as a removal.

'Mathlib/LinearAlgebra/RootSystem/GeckConstruction.lean' was renamed to
'Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Relations.lean' (R050),
but the similarity 50% is less than the expected threshold of 100%.
          We treat this file as a removal.

'Mathlib/RingTheory/DedekindDomain/Ideal.lean' was renamed to
'Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean' (R060),
but the similarity 60% is less than the expected threshold of 100%.
          We treat this file as a removal.

'Mathlib/Algebra/Group/FiniteSupport.lean'

[Jireh Loreaux]

Did someone fix Projection already?

[Damiano Testa]

Sorry, I copy-pasted the ones that were not classed as renames. These are the removals in the last 600 commits.

• #create_deprecated_module "Mathlib/Analysis/InnerProductSpace/Projection.lean"

• #create_deprecated_module "Mathlib/Algebra/Notation/Pi.lean"

• #create_deprecated_module "Mathlib/RingTheory/DedekindDomain/Ideal.lean"

• #create_deprecated_module "Mathlib/CategoryTheory/Monoidal/Limits.lean" rename_to
    "Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean"

• #create_deprecated_module "Mathlib/Algebra/Group/FiniteSupport.lean"

[Jireh Loreaux]

Is the script detecting renames based on the git history?

[Damiano Testa]

Yes, in fact, it reads what git thinks the percentage of a change being a rename and acts accordingly.

[Damiano Testa]

I set the threshold for "counts as a rename" to be "100%", but this was just me trying to be conservative.

[Damiano Testa]

Basically, the script is a way of getting Lean to read off the appropriate git commands to figure out which files existed in the past, no longer exist now and whether they should be considered files that were removed or files that were renamed.

[Damiano Testa]

Based on this data, then the command can write the deprecated module accordingly: copy the imports for a removed file, import the renamed module for a rename.

[Damiano Testa]

I tried to make the command already have a clear "suggestion" of what to do, since it is my intention to use this in a completely automated way. However, before getting there, I wanted to have something where you could confirm that simply clicking through the suggestion consistently produced the correct output, before automating the "click the unique suggestion" and stick it into CI.

[Jireh Loreaux]

#28417 deprecates Projection

[Jireh Loreaux]

@Damiano Testa Per your GitHub comment:

You went for making it import the files into which the removed file was scattered, rather than the direct imports of the original file itself. While this is certainly a good choice, I wonder how to make the deprecated_module automation pick this up. The script would have used the imports of the deleted file.

I'm not sure why using the direct imports of the original file would make any sense (no offense intended here). Indeed, suppose the file Bar.lean is split into two files Bar1.lean and Bar2.lean, and the original imports of Bar.lean consists of onlyFoo.lean. Then any downstream user who had been importing Bar.lean for some declaration bar in that file will still be left with "unknown identifier bar". Sure, they'll also get "Bar.lean is deprecated", but replacing it with Foo.lean won't help and they'll be stuck without hunting through the git history.

[Jireh Loreaux]

As for how to pick this up automatically: maybe if git detects that the file is not a rename but a deletion, then the command suggests all other files edited in that commit (with a diff of more than 5, number TBD, lines to avoid import changes to other random files in the original commit)?

[Robin Carlier]

#28423 add the deprecation notice to Mathlib/CategoryTheory/Monoidal/Limits.lean.

[Bryan Gin-ge Chen]

@Kevin Buzzard pointed out in a comment that #28948 moved several files and there was no follow-up deprecation PR. I suspect that this particular case may just be a case of bad timing, since @Michael Rothgang is now on vacation, but maybe we should try and push again to the automation for this working? I should have some time in a day or two if we need some more bots written, etc. It looks like #24917 is now on awaiting-author, but does it still need a review?

[Damiano Testa]

I will take a look now at the PR.

[Damiano Testa]

The PR makes module deprecation "semi-automatic": with very little input, it guides through the creation of a deprecated module.

[Damiano Testa]

Making it fully automatic would not be hard (and was the initial goal), but it is not easy to get the deprecation command right, so I wanted to make it "supervised" for a bit, so that bugs and issues could be ironed out, before integrating it into CI.

[Damiano Testa]

Ok, having reviewed the unresolved comments, they do not seem to me as bug reports.

[Damiano Testa]

I think that testing this semi-automation would be easier if the command were in mathlib.

[Damiano Testa]

Moreover, the command needs to be called by a human, as it currently does nothing completely autonomously.

[Damiano Testa]

Let me see what it would suggest for the missing deprecations from #28948.

[Bryan Gin-ge Chen]

OK, I'm about to head out for a bit so I have delegated with the understanding that this will probably evolve after more testing / integration with automation.

[Damiano Testa]

#29209 is the deprecating PR. I on purpose had as little input as possible into generating it.

[Damiano Testa]

If it looks correct, I'll add some documentation to the deprecating automation and will merge that PR! :slight_smile:

[Kevin Buzzard]

Thanks so much Damiano!

[Michael Rothgang]

To add my two cents: #2491 had basically looked good to me: the remaining points were nits/requests for documentation, and there was one bug that would sometimes make the command do the wrong thing. Iterating on this in-tree is fine with me.

[Michael Rothgang]

I'd rather have this automation at all than having to manually enact it :-)

[Damiano Testa]

I added the deprecations for the files from #28909 to #29209. This uncovered a bug in the old program that I fixed. If someone can confirm that the deprecations are correct (or at least look reasonable), then I will go ahead and merge the (fixed up) script.

[Damiano Testa]

Kevin, the module deprecations have now been merged: let me know if there are some further issues!

[Damiano Testa]

I also created #29293 semi-automatically, adding deprecations for module changes arising from the last 50 commits.

• #29263 and #29267: @Jireh Loreaux I see that you already prepared #29264, so this is a great opportunity to see how the automated deprecation compares to the manual one!

• #25790: @Jeremy Tan does the deprecation in the PR above look correct to you?

[Damiano Testa]

Ultimately, these PRs should be generated entirely automatically, but right now, I am still testing the process manually, to make sure that we can trust a bot to do it! :slight_smile:

[Jireh Loreaux]

sorry, I didn't see this and I already merged my deprecation PRs.

[Jireh Loreaux]

@Damiano Testa I don't think #25790 is the correct PR. Did you mean #29125 ?

[Jireh Loreaux]

#29293 looks correct to me (for all the deprecations, not just mine).

[Jireh Loreaux]

Once #29323 is merged you'll have another testbed for your script.

[Jireh Loreaux]

@Damiano Testa where is the branch with the #create_deprecated_module command? I couldn't find it.

[Damiano Testa]

The command is on master now: scripts/create_deprecated_module` or something like that.

[Damiano Testa]

(I'm on mobile)

[Jireh Loreaux]

oh I see, thanks!

[Eric Wieser]

Eric Wieser said:

I've just seen a strong reason to do this in a separate PR; if you don't the conflicts downstream are not automatically resolved

It looks like I may have overestimated git here; I think to actually benefit from this data, you need to first merge the commit just before the deprecated_modules were added, then merge master

[Eric Wieser]

(in that, I have a datapoint where a direct merge of master fails, but a merge of some_deprecated_module_sha^ then master works)

[Eric Wieser]

So either we should encourage the use of git imerge, or we should batch up all the deprecated module creation to do just once a month, so it's easy to just merge those commits

[Ruben Van de Velde]

✖ [2300/2314] Running Mathlib.Data.Complex.Norm
error: no such file or directory (error code: 2)

[Eric Wieser]

A missing module deprecation, I guess?

[Ruben Van de Velde]

Indeed (again)

[Damiano Testa]

#29672

[Damiano Testa]

Once again, an almost auto-generated PR. I was only guiding the deprecations by telling it which of the files that have been removed recently should have been deprecated (and I aimed for the ones in the PR that removed the ones that Ruben discovered).

[Damiano Testa]

I have not even looked at the autogenerated files before making the PR!

[Eric Wieser]

@Kim Morrison, should we move the 4.23.0 tag to point after Damiano's PR?

[Eric Wieser]

Or is it too late once the tag is created? (It's certainly too late once the bors'd #29671 lands)

[Damiano Testa]

(As in the past, I had forgotten about running mk_all. :man_facepalming:)

[Bryan Gin-ge Chen]

Couldn't we cherry-pick Damiano's commit onto the 4.23.0 tag, or have we promised somewhere that it's always a commit on master?

[Eric Wieser]

I think the bigger question is whether we've promised that 4.23.0 doesn't move

[Jireh Loreaux]

Isn't this kind of thing what the third digit is for?

[Jireh Loreaux]

Oh no, it needs to match Lean, nevermind.

[Bryan Gin-ge Chen]

Whatever the answer is re: the 4.23.0 tag (and 4.x.y tags in general), we really need to document it here; and possibly the README too.

[Kim Morrison]

In this case, it seems certainly too minor to warrant cherry-picking or moving the tag.

We can discuss elsewhere future policy for modifying these tags.

[Ruben Van de Velde]

Note to self for next month:

1. Check out master and get cache
2. Run git rev-list v4.X.0... | wc -l
3. Copy the number to scripts/create_deprecated_modules.lean line 374
4. Apply the suggestions on #find_deleted_files
5. Apply the suggestions on each of the #create_deprecated_module commands
6. Manually git add each of the created files
7. For each added file, look up the commit where it was removed and check if the imports from the command make sense, and fix if needed
8. Run mk_all
9. Run lake build
10. commit, push and make pr

[Michael Rothgang]

Step 8 is also done on CI: if you forget to make something a module, lake build will fail (as Mathlib.lean cannot import non-modules)

[Ruben Van de Velde]

Okay, but then I need step 11: wait for ci :)

[Michael Rothgang]

Sure - you get to pick your poison.

[Ruben Van de Velde]

Which I need anyway

[Michael Rothgang]

Though: can you lake build locally? Hopefully, these are only new files which should be quick to import, right?

[Michael Rothgang]

(Assuming you have full cache for mathlib, of course.)

[Ruben Van de Velde]

Yeah, good point

[Damiano Testa]

Ruben, thank you very much for this!

I am really grateful that you worked this out, so that now there is a concrete suggestion for further automation!

[Ruben Van de Velde]

That would be ideal :)