fix: display deprecation warning for simp lemmas on the lemma name

[joneugster]

Closes #4452

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e33c32fb00e7b2a01c6a7f186c18a7c97f54a635 --onto bedcbfcfeed429428c3e7f008b6984fc8c2b2b76. (2024-06-13 20:37:40)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e33c32fb00e7b2a01c6a7f186c18a7c97f54a635 --onto f237fb67ebe344b7e26f67cf7c35b1a69dcefdc9. (2024-06-17 10:27:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e33c32fb00e7b2a01c6a7f186c18a7c97f54a635 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-17 12:16:03)

[tydeu]

Suggested change

	match (← withRef arg do resolveSimpIdTheorem? term) with
	match (← withRef term do resolveSimpIdTheorem? term) with

It seems more reasonable to use the term itself rather than the whole arg (which potentially includes the inversion arrow). Alternatively, the withRef could be integrated into resolveSimpIdTheorem? itself, which might be even better.

[joneugster]

Overlooked the second suggestion, but just addressed that now, see below.

[adomani]

In the Zulip chat it was suggested to add a test. Would this (updated to the correct message) work?

import Lean.Elab.Command

@[deprecated]
theorem hi : True := .intro

open Lean Elab.Command
elab "msgs_lines " cmd:command : command => do
  elabCommand cmd
  let msgs := (← get).messages.unreported.toList
  if let [m] := msgs then logInfo m!"{(m.pos, m.endPos)}"

/--
warning: `hi` has been deprecated
---
info: (⟨20, 2⟩, some (⟨22, 3⟩))
-/
#guard_msgs in
msgs_lines
example : True := by
  simp [
    hi
  ]

[semorrison]

In the Zulip chat it was suggested to add a test. Would this (updated to the correct message) work?

Haha, I like it. The traditional way is to do it like the tests in tests/lean/interactive/.

[joneugster]

The traditional way is to do it like the tests in tests/lean/interactive/.

@semorrison I did add a test to the best of my knowledge (as 4448.lean and 4448.lean.expected.out), not following tests/lean/interactive/ but other tests in tests/lean/, is this the correct way?

EDIT: I guess the failing CI in af33b4a suggests it does indeed work :D

[joneugster]

@semorrison I managed to get the tests correctly :) I don't think I can remove the awaiting-author label, so I assume the right thing is to ping you instead?

[nomeata]

It seems that this was now fixed by #4484, please re-open if I am confused. Thanks for helping, though!

[joneugster]

Absolutely, thanks for the fix!

[adomani]

I also tried the web-server and I can still see the old simp-underlining. Would you mind also adding dsimp to the test, just to make sure that the same modifications fix both? Thanks!

[joneugster]

I also tried the web-server and I can still see the old simp-underlining.

Did you try the "Nightly" version of the webeditor? (go to settings and change the project) It seems to be as intended:
MWE on web editor nightly

[adomani]

Ah, no, I did not know that this was possible! I can confirm that on the "nightly", the issue that I had raised is resolved, both for simp and for dsimp!

I am not really able to comment whether this is the "right" solution, but I would be very happy if this behaviour became standard! Thanks!

[adomani]

Oh, I realize now that you are saying that this already is the behaviour, it just has not trickled down to Mathlib! Anyway, this is great, thanks!

[joneugster]

exactly, I assume that means it'll be in v4.10.0 and the corresponding rcs