Merge main into nightly-testing

leanprover-community · May 21, 2024 · 8a26337 · 8a26337
2 parents 27343fe + f3e6d5d
commit 8a26337
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/Batteries/Tactic/Alias.lean b/Batteries/Tactic/Alias.lean
@@ -63,9 +63,11 @@ def setDeprecatedTarget (target : Name) (arr : Array Attribute) : Array Attribut
   StateT.run (m := Id) (s := false) do
     arr.mapM fun s => do
       if s.name == `deprecated then
-        if let `(deprecated| deprecated%$tk) := s.stx then
+        if let `(deprecated| deprecated%$tk $[$desc:str]? $[(since := $since)]?) := s.stx then
           set true
-          pure { s with stx := Unhygienic.run `(deprecated| deprecated%$tk $(mkCIdent target)) }
+          let stx := Unhygienic.run
+            `(deprecated| deprecated%$tk $(mkCIdent target) $[$desc:str]? $[(since := $since)]?)
+          pure { s with stx }
         else pure s
       else pure s
 

diff --git a/test/alias.lean b/test/alias.lean
@@ -13,12 +13,15 @@ theorem foo : 1 + 1 = 2 := rfl
 alias foo1 := foo
 @[deprecated] alias foo2 := foo
 @[deprecated foo2] alias _root_.B.foo3 := foo
+@[deprecated foo2 "it was never a good idea anyway" (since := "last thursday")] alias foo4 := foo
 
 example : 1 + 1 = 2 := foo1
 /-- warning: `A.foo2` has been deprecated, use `A.foo` instead -/
 #guard_msgs in example : 1 + 1 = 2 := foo2
 /-- warning: `B.foo3` has been deprecated, use `A.foo2` instead -/
 #guard_msgs in example : 1 + 1 = 2 := B.foo3
+/-- warning: it was never a good idea anyway -/
+#guard_msgs in example : 1 + 1 = 2 := foo4
 
 /-- doc string for bar -/
 def bar : Nat := 5