Thank you for the deprecation warnings!

Stream: mathlib4

[Geoffrey Irving]

This time when I updated mathlib, most of the functions that have been renamed come with deprecation warnings that say what the new function is. This has made this most recent upgrade experience far more pleasant than the last time. Thank you!

One feature request: it would be cool if the deprecation warnings produced clickable things in VSCode that did the substitution, since often just doing the name replace works (and even if it doesn't one can then edit to fix).

[Damiano Testa]

I have not really thought about this, but it might be tricky to get the substitution to work automatically, mostly due to dot-notation and what the new name should look like.

Someone else may have a better answer, though!

[Damiano Testa]

(I am not saying that it is impossible, but that a simple-minded replacement would not "Just work".)

[Richard Copley]

If it's purely a name change In some cases, as in

@[deprecated] alias oldname := newname

there will indeed be a code action (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/machineApplicableDeprecated.20tag.20attribute).

[Damiano Testa]

@Richard Copley the link that you shared highlights that the auto-deprecated script that I used produces the wrong syntax for automatic replacement to work.

@Geoffrey Irving, if your deprecated lemmas were of the op_norm-form, then auto-replacement might have worked better if I had understood how this worked...

[Damiano Testa]

Hopefully, #10302 uses the correct syntax and allows auto-replacement of the deprecated op_norm statements.

[Geoffrey Irving]

Very cool, thank you! Yep, getting the simple cases right gets nearly all of the value.

[Damiano Testa]

In case someone comes here, with the PR, the deprecation code action works with the lemmas that were auto-deprecated. However, even the deprecation does not seem to work if you use a deprecated lemma with dot-notation:

import Std.Tactic.Alias

@[deprecated] alias Nat.sup := Nat.succ_pos

-- code action works
example {m : Nat} : 0 < m.succ := Nat.sup m

open Nat in
-- code action works
example {m : Nat} : 0 < m.succ := sup m

-- no deprecation notice
example {m : Nat} : 0 < m.succ := m.sup

[Ruben Van de Velde]

Not even a warning?

[Damiano Testa]

No, not even a warning.

[Johan Commelin]

Sounds like that should be a bug report for core.

[Damiano Testa]

Filed as issue #3270

[Josha Dekker]

There was a deprecation warning in Topology/Compactness/Lindelof which I tried to fix by carrying out the suggested change (from subset_trans to embedding_inclusion), but this involved more than just replacing the name of the result, as the result from embedding_inclusion was an Embedding.

My build on #10376 failed when I committed without fixing the deprecation warning, so in order to get my PR to build, I would've been forced to figure out how to do the proof with the intermediate Embedding step, which feels like it adds quite some overhead if you want to quickly add another result which happens to be in the same file as the deprecated step. In this case, aesop quickly gave me a different proof that didn't use embedding.

My question is, is this efficient behaviour, that the build fails when I don't change a deprecated step that doesn't have anything to do with my contribution? Or am I misinterpreting what happened?

[Ruben Van de Velde]

I don't think a new warning should come up and block you if you make an unrelated change, if I understand you correctly

[Josha Dekker]

Ruben Van de Velde said:

I don't think a new warning should come up and block you if you make an unrelated change, if I understand you correctly

Yes, exactly, that would be what I thought as well. What happened was the following:

The warning was there when I opened the file in VS code. The build failed on my first commit because I forgot to check the lint, but then the build failed on my second commit, due to the presence of a deprecated function in the file, which was unrelated to my change

[Ruben Van de Velde]

Ah, I see what happened

[Ruben Van de Velde]

The code on master uses _root_.subset_trans which isn't deprecated. You added a new import, which caused subset_trans to resolve to TopologicalSpace.subset_trans instead, and this one is deprecated.

[Ruben Van de Velde]

So you could make this change instead:

-  have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i := fun _ is ↦ subset_trans (subset_biUnion_of_mem is) hUcover
+  have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i := fun _ is ↦
+    _root_.subset_trans (subset_biUnion_of_mem is) hUcover

[Josha Dekker]

Okay, that makes sense, I'll fix that line as I think it is more elegant. Would it be good to have something (in general) that avoids that fun resolves to something like A.fun rather than B.fun if the former is deprecated? Or is this horribly complicated to add? I guess it would prevent issues like the one I just ran into.

[Damiano Testa]

The systematic use of deprecated in Mathlib is very recent. There are several improvements that would be great, not necessarily hard to implement. There just has not been enough time to really write them, I think.

[Ruben Van de Velde]

I'm not convinced that deprecation should affect name resolution. If this particular theorem hadn't been deprecated, you'd also have hit a weird error because the signature no longer matched

[Kyle Miller]

In case people aren't aware of it, Mathlib Changelog is a useful tool when you need to figure out what happened to some declaration when you're upgrading.