Bug in `deprecate to`

Stream: mathlib4

[Michael Rothgang]

It seems I found a bug in deprecate to. Here's an MWE:

import Mathlib

open MeasureTheory

deprecate to Gamma_integrand_intervalIntegrable
private theorem Gamma_integrand_interval_integrable (s : ℂ) {X : ℝ} (hs : 0 < s.re) (hX : 0 ≤ X) :
    IntervalIntegrable (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) volume 0 X := by
  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hX]
  exact IntegrableOn.mono_set (Complex.GammaIntegral_convergent hs) Set.Ioc_subset_Ioi_self

Running this on the playground yields an error; in VS Code, the try this suggestion produces

private theorem Gamma_integrand_intervalIntegrable (s : ℂ) {X : ℝ} (hs : 0 < s.re) (hX : 0 ≤ X) :
    IntervalIntegrable (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) volume 0 X :=
  by
  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hX]
  exact IntegrableOn.mono_set (GammaIntegral_convergent hs) Ioc_subset_Ioi_self

@[deprecated (since := "2024-07-22")]
alias [anonymous] := Gamma_integrand_intervalIntegrable

which is off in two ways: the lemma name is missing, and the by is printed in the wrong place. CC @Damiano Testa

[Damiano Testa]

It looks like the modifier private confuses deprecate to: the name appears correctly filled in without private.

[Damiano Testa]

The formatting is an unfortunate consequence of the fact that the command relies on the pretty-printer for reproducing the declarations. That could possibly be avoided by editing the actual lines of the current file, but that may run into problems when the saved content is different from the currently edited file.

[Damiano Testa]

Btw, is there really the need to deprecate a private lemma? :smile:

[Michael Rothgang]

Damiano Testa said:

Btw, is there really the need to deprecate a private lemma? :smile:

Good question! I don't mind removing the alias...

[Floris van Doorn]

Let's not deprecate private lemmas

[Damiano Testa]

Btw, the error in the playground happens since the code is secretly running a shell command to get the current date. This makes the playground unhappy. You can add a string to override this:

deprecate to ... "string"
theorem ...

and string will be the date in since.