feat: add deprecated_syntax

src/Lean/Elab/BuiltinCommand.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Reduce
 public import Lean.Elab.Eval
 public import Lean.Elab.Command
+import Lean.Elab.DeprecatedSyntax
 public import Lean.Elab.Open
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
@@ -706,4 +707,15 @@ where
     let env ← getEnv
     IO.eprintln (← env.dbgFormatAsyncState)
 
+@[builtin_command_elab Parser.Command.deprecatedSyntax] def elabDeprecatedSyntax : CommandElab := fun stx => do
+  let id := stx[1]
+  let kind ← liftCoreM <| checkSyntaxNodeKindAtNamespaces id.getId (← getCurrNamespace)
+  let text? := if stx[2].isNone then none else stx[2][0].isStrLit?
+  let since? := if stx[3].isNone then none else stx[3][3].isStrLit?
+  if since?.isNone then
+    logWarning "`deprecated_syntax` should specify the date or library version at which the \
+      deprecation was introduced, using `(since := \"...\")`"
+  modifyEnv fun env =>
+    deprecatedSyntaxExt.addEntry env { kind, text?, since? }
+
 end Lean.Elab.Command

src/Lean/Elab/DeprecatedSyntax.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.MonadEnv
+public import Lean.Linter.Basic
+public import Lean.Elab.Util
+
+public section
+
+namespace Lean.Linter
+
+register_builtin_option linter.deprecatedSyntax : Bool := {
+  defValue := true
+  descr := "if true, generate warnings when deprecated syntax is used"
+}
+
+end Lean.Linter
+
+namespace Lean.Elab
+
+/-- Entry recording that a syntax kind has been deprecated. -/
+structure SyntaxDeprecationEntry where
+  /-- The syntax node kind that is deprecated. -/
+  kind : SyntaxNodeKind
+  /-- Optional deprecation message. -/
+  text? : Option String := none
+  /-- Optional version or date at which the syntax was deprecated. -/
+  since? : Option String := none
+
+builtin_initialize deprecatedSyntaxExt :
+    SimplePersistentEnvExtension SyntaxDeprecationEntry (NameMap SyntaxDeprecationEntry) ←
+  registerSimplePersistentEnvExtension {
+    addImportedFn := mkStateFromImportedEntries (fun m e => m.insert e.kind e) {}
+    addEntryFn := fun m e => m.insert e.kind e
+  }
+
+/--
+Check whether `stx` is a deprecated syntax kind, and if so, emit a warning.
+
+If `macroStack` is non-empty, the warning is attributed to the macro call site rather than the
+syntax itself.
+-/
+def checkDeprecatedSyntax [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
+    [AddMessageContext m] [MonadRef m] (stx : Syntax) (macroStack : MacroStack) : m Unit := do
+  let env ← getEnv
+  let kind := stx.getKind
+  if let some entry := (deprecatedSyntaxExt.getState env).find? kind then
+    let extraMsg := match entry.text? with
+      | some text => m!": {text}"
+      | none => m!""
+    match macroStack with
+    | { before := macroStx, .. } :: _ =>
+      withRef macroStx do
+        Linter.logLintIf Linter.linter.deprecatedSyntax stx
+          m!"macro '{macroStx.getKind}' produces deprecated syntax '{kind}'{extraMsg}"
+    | [] =>
+      Linter.logLintIf Linter.linter.deprecatedSyntax stx
+        m!"syntax '{kind}' has been deprecated{extraMsg}"
+
+end Lean.Elab

src/Lean/Elab/Quotation/Precheck.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Elab.Quotation.Util
+import Lean.Elab.DeprecatedSyntax
 
 public section
 
@@ -56,6 +57,14 @@ unsafe builtin_initialize precheckAttribute : KeyedDeclsAttribute Precheck ←
   }
 
 partial def precheck : Precheck := fun stx => do
+  -- Check for deprecated syntax kinds in quotations
+  if let some entry := (deprecatedSyntaxExt.getState (← getEnv)).find? stx.getKind then
+    let extraMsg := match entry.text? with
+      | some text => m!": {text}"
+      | none => m!""
+    withRef stx do
+      Linter.logLintIf Linter.linter.deprecatedSyntax stx
+        m!"quotation uses deprecated syntax '{stx.getKind}'{extraMsg}"
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
     if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; pure true) (fun _ => pure false) then
       return

src/Lean/Elab/Tactic/Basic.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Util
 public import Lean.Elab.Term
+import Lean.Elab.DeprecatedSyntax
 import Init.Omega
 
 public section
@@ -192,6 +193,7 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
         Term.withoutTacticIncrementality true <| withTacticInfoContext stx do
           stx.getArgs.forM evalTactic
       else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
+        checkDeprecatedSyntax stx (← readThe Term.Context).macroStack
         let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
         let macros  := macroAttribute.getEntries (← getEnv) stx.getKind
         if evalFns.isEmpty && macros.isEmpty then

src/Lean/Elab/Term/TermElabM.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Coe
 public import Lean.Util.CollectLevelMVars
 public import Lean.Linter.Deprecated
+import Lean.Elab.DeprecatedSyntax
 public import Lean.Elab.Attributes
 public import Lean.Elab.Level
 public import Lean.Elab.PreDefinition.TerminationHint
@@ -1794,6 +1795,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     withTraceNode `Elab.step (fun _ => return m!"expected type: {expectedType?}, term\n{stx}")
       (tag := stx.getKind.toString) do
     checkSystem "elaborator"
+    checkDeprecatedSyntax stx (← read).macroStack
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>

src/Lean/Parser/Command.lean

@@ -620,6 +620,15 @@ declaration signatures.
 /-- Debugging command: Prints the result of `Environment.dumpAsyncEnvState`. -/
 @[builtin_command_parser] def dumpAsyncEnvState := leading_parser
   "#dump_async_env_state"
+/--
+Mark a syntax kind as deprecated. When this syntax is elaborated, a warning will be emitted.
+
+```
+deprecated_syntax Lean.Parser.Term.let_fun "use `have` instead" (since := "2026-03-18")
+```
+-/
+@[builtin_command_parser] def deprecatedSyntax := leading_parser
+  "deprecated_syntax " >> ident >> optional (ppSpace >> strLit) >> optional (" (" >> nonReservedSymbol "since" >> " := " >> strLit >> ")")
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 /--

tests/elab/deprecated_syntax.lean

@@ -0,0 +1,52 @@
+-- Enable the deprecated syntax linter (test framework disables all linters)
+set_option linter.deprecatedSyntax true
+
+-- Test 1: Direct usage of deprecated term syntax → warning
+deprecated_syntax Lean.Parser.Term.let_fun "use `have` instead" (since := "2026-03-24")
+
+-- Note: the paren macro expands to the inner expression, so the warning
+-- is attributed to the paren macro call site
+#check (let_fun x := 1; x)
+
+-- Test 2: Macro that expands to deprecated syntax → warning at macro call site
+syntax "my_wrapper " : term
+macro_rules | `(my_wrapper) => `(let_fun x := 1; x)
+
+#check (my_wrapper)
+
+-- Test 3: set_option linter.deprecatedSyntax false suppresses warnings
+set_option linter.deprecatedSyntax false in
+#check (let_fun x := 1; x)
+
+-- Test 4: Non-deprecated syntax → no warning
+#check (42 : Nat)
+
+-- Test 5: deprecated_syntax for a tactic
+syntax "myDepTac" : tactic
+macro_rules | `(tactic| myDepTac) => `(tactic| trivial)
+
+deprecated_syntax tacticMyDepTac "use `trivial` instead" (since := "2026-03-24")
+
+example : True := by myDepTac
+
+-- Test 6: Quotation precheck warns at macro definition time
+-- Define a custom syntax, give it a macro expansion, then deprecate it
+syntax "oldThing" : term
+macro_rules | `(oldThing) => `(42)
+deprecated_syntax termOldThing "use `42` instead" (since := "2026-03-24")
+
+-- A macro whose RHS quotation uses the deprecated syntax → warning at definition site
+syntax "usesOld " : term
+macro_rules | `(usesOld) => ``(oldThing)
+
+-- Test 7: set_option linter.deprecatedSyntax false suppresses quotation precheck warning
+syntax "usesOld2 " : term
+set_option linter.deprecatedSyntax false in
+macro_rules | `(usesOld2) => ``(oldThing)
+
+-- Test 8: Quotation that does NOT use deprecated syntax → no warning
+syntax "usesNew " : term
+macro_rules | `(usesNew) => ``(42)
+
+-- Test 9: missing since emits a warning
+deprecated_syntax Lean.Parser.Term.show

tests/elab/deprecated_syntax.lean.out.expected

@@ -0,0 +1,20 @@
+deprecated_syntax.lean:9:8-9:25: warning: macro 'Lean.Parser.Term.paren' produces deprecated syntax 'Lean.Parser.Term.let_fun': use `have` instead
+
+Note: This linter can be disabled with `set_option linter.deprecatedSyntax false`
+have x := 1;
+x : Nat
+deprecated_syntax.lean:15:8-15:18: warning: macro 'termMy_wrapper' produces deprecated syntax 'Lean.Parser.Term.let_fun': use `have` instead
+
+Note: This linter can be disabled with `set_option linter.deprecatedSyntax false`
+have x := 1;
+x : Nat
+have x := 1;
+x : Nat
+42 : Nat
+deprecated_syntax.lean:30:21-30:29: warning: syntax 'tacticMyDepTac' has been deprecated: use `trivial` instead
+
+Note: This linter can be disabled with `set_option linter.deprecatedSyntax false`
+deprecated_syntax.lean:40:31-40:39: warning: quotation uses deprecated syntax 'termOldThing': use `42` instead
+
+Note: This linter can be disabled with `set_option linter.deprecatedSyntax false`
+deprecated_syntax.lean:52:0-52:39: warning: `deprecated_syntax` should specify the date or library version at which the deprecation was introduced, using `(since := "...")`