Rename in Batteries

Stream: nightly-testing

[Damiano Testa]

In batteries#861 I changed a namespace from Std to Batteries. I now checked that in Mathlib this will likely affect what is below.

Mathlib/Mathport/Notation.lean:615:initialize Std.Linter.UnreachableTactic.addIgnoreTacticKind ``«notation3»
Mathlib/Tactic/Hint.lean:53:  Std.Linter.UnreachableTactic.ignoreTacticKindsRef.modify fun s => s.insert ``registerHintStx
Mathlib/Tactic/Says.lean:135:initialize Std.Linter.UnreachableTactic.addIgnoreTacticKind `Mathlib.Tactic.Says.says

Which branch should I update in Mathlib to use the correct namespace?

[Kim Morrison]

@Damiano Testa, already done on #14145, and awaiting your approval. :-)

[Kim Morrison]

changes to Batteries just require a PR to mathlib that runs lake update and fixes the problems.

[Kim Morrison]

as of today there is a working bot that tries to do this itself

[Kim Morrison]

the component that posts to zulip if the PR fails is not yet (visibly?) working

[Damiano Testa]

Ok, I am happy to approve the changes, but I do not understand the implications of removing BinaryHeap.

[Kim Morrison]

It moved to batteries.

[Damiano Testa]

Ah, great!

[Damiano Testa]

"delegated merge"!

[Damiano Testa]

Could the flow have been: add a deprecation either in Batteries or in Mathlib, run the autocorrecting script that fixes deprecations? Is there some reason not to do that, other than the script has not been tested much?

[Kim Morrison]

For what?

[Damiano Testa]

For the rename.

[Kim Morrison]

BinaryHeap?

[Damiano Testa]

No, the linter rename.

[Kim Morrison]

oh, the Std/Batteries

[Kim Morrison]

yes, ideally we would have added a @[deprecated (since := ...)] alias ...

[Damiano Testa]

In this case it was not a lot of work, I imagine, but in general I can imagine that it is tedious.

[Kim Morrison]

Yes, and I think everyone is in furious agreement that more deprecation statements is better than less. :-)

[Damiano Testa]

Ok, I can try testing more the deprecation automation, maybe also looking into incorporating into lake refactor.

[Damiano Testa]

But currently, the standalone should "work", in the sense that I did some small number of tests and it seems to work.

[Damiano Testa]

Would it make sense to think about whether something like PR summary also had a "Did you want to deprecate ...?" section?

[Johan Commelin]

As part of the diff?

[Damiano Testa]

Yes, thinking a little about what and how to flag changes...

[Michael Rothgang]

Damiano Testa said:

Would it make sense to think about whether something like PR summary also had a "Did you want to deprecate ...?" section?

I think automating this step would be great, in principle! I haven't thought much about the details.