feat: add deprecated_syntax (#13108)

This PR adds a `deprecated_syntax` command that marks syntax kinds as
deprecated. When deprecated syntax is elaborated (in terms, tactics, or
commands), a linter warning is emitted. The warning is also emitted
during quotation precheck when a macro definition uses deprecated syntax
in its expansion.

The `deprecated_syntax` command takes a syntax node kind, an optional
message, and a `(since := "...")` clause. Deprecation warnings correctly
attribute the warning to macro call sites when the deprecated syntax is
produced by macro expansion, including through nested macro chains.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

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
@@ -715,4 +716,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/Command.lean

@@ -10,6 +10,7 @@ public import Lean.Meta.Diagnostics
 public import Lean.Elab.Binders
 public import Lean.Elab.Command.Scope
 public import Lean.Elab.SetOption
+import Lean.Elab.DeprecatedSyntax
 public meta import Lean.Parser.Command
 
 public section
@@ -468,6 +469,7 @@ where go := do
       else withTraceNode `Elab.command (fun _ => return stx) (tag :=
         -- special case: show actual declaration kind for `declaration` commands
         (if stx.isOfKind ``Parser.Command.declaration then stx[1] else stx).getKind.toString) do
+        checkDeprecatedSyntax stx (← read).macroStack
         let s ← get
         match (← liftMacroM <| expandMacroImpl? s.env stx) with
         | some (decl, stxNew?) =>

src/Lean/Elab/DeprecatedSyntax.lean

@@ -0,0 +1,71 @@
+/-
+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.deprecated.syntax : 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, .. } :: { before := callerStx, .. } :: _ =>
+      let expandedFrom :=
+        if callerStx.getKind != macroStx.getKind then
+          m!" (expanded from '{callerStx.getKind}')"
+        else m!""
+      Linter.logLintIf Linter.linter.deprecated.syntax macroStx
+        m!"macro '{macroStx.getKind}'{expandedFrom} produces deprecated syntax '{kind}'{extraMsg}"
+    | { before := macroStx, .. } :: [] =>
+      Linter.logLintIf Linter.linter.deprecated.syntax macroStx
+        m!"macro '{macroStx.getKind}' produces deprecated syntax '{kind}'{extraMsg}"
+    | [] =>
+      Linter.logLintIf Linter.linter.deprecated.syntax 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.deprecated.syntax 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/Tactic/Grind/Config.lean

@@ -7,6 +7,8 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.ConfigSetter
+import Lean.Elab.DeprecatedSyntax  -- shake: skip (workaround for `mkConfigSetter` failing to interpret `deprecatedSyntaxExt`, to be fixed)
+
 public section
 namespace Lean.Elab.Tactic.Grind
 

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

@@ -622,6 +622,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"
 /--

stage0/src/stdlib_flags.h

@@ -11,7 +11,7 @@ options get_default_options() {
     opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with

tests/elab/deprecated_syntax.lean

@@ -0,0 +1,84 @@
+-- Enable the deprecated syntax linter (test framework disables all linters)
+set_option linter.deprecated.syntax 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
+  It will not warn at macro definition, as it is defined via
+  single backtick and hence does not trigger a pre-check.
+-/
+syntax "my_wrapper " : term
+macro_rules | `(my_wrapper) => `(let_fun x := 1; x)
+
+#check (my_wrapper)
+
+-- Test 2b: Nested macros — A expands to B, B expands to deprecated syntax.
+-- Warning names immediate producer (innerMacro) and its caller (outerMacro).
+syntax "innerMacro " : term
+macro_rules | `(innerMacro) => `(let_fun x := 1; x)
+syntax "outerMacro " : term
+macro_rules | `(outerMacro) => `(innerMacro)
+
+-- Use `let` binding to avoid parens adding another macro layer
+def nested_test := outerMacro
+
+-- Test 3: set_option linter.deprecated.syntax false suppresses warnings
+set_option linter.deprecated.syntax 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.deprecated.syntax false suppresses quotation precheck warning
+syntax "usesOld2 " : term
+set_option linter.deprecated.syntax 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: deprecated_syntax for a command — direct usage
+syntax "myDepCmd " : command
+macro_rules | `(myDepCmd) => `(#check 42)
+
+deprecated_syntax commandMyDepCmd "use `#check` instead" (since := "2026-03-24")
+
+myDepCmd
+
+-- Test 9b: Macro that expands to deprecated command → warning at macro call site
+syntax "myWrapperCmd " : command
+macro_rules | `(myWrapperCmd) => `(myDepCmd)
+
+myWrapperCmd
+
+-- Test 9c: set_option linter.deprecated.syntax false suppresses command warning
+set_option linter.deprecated.syntax false in
+myDepCmd
+
+-- Test 10: missing since emits a warning
+deprecated_syntax Lean.Parser.Term.show

tests/elab/deprecated_syntax.lean.out.expected

@@ -0,0 +1,32 @@
+deprecated_syntax.lean:9:7-9:26: 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.deprecated.syntax false`
+have x := 1;
+x : Nat
+deprecated_syntax.lean:19:8-19:18: warning: macro 'termMy_wrapper' (expanded from '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.deprecated.syntax false`
+have x := 1;
+x : Nat
+deprecated_syntax.lean:29:19-29:29: warning: macro 'termInnerMacro' (expanded from 'termOuterMacro') produces deprecated syntax 'Lean.Parser.Term.let_fun': use `have` instead
+
+Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
+have x := 1;
+x : Nat
+42 : Nat
+deprecated_syntax.lean:44:21-44:29: warning: syntax 'tacticMyDepTac' has been deprecated: use `trivial` instead
+
+Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
+deprecated_syntax.lean:54:31-54:39: warning: quotation uses deprecated syntax 'termOldThing': use `42` instead
+
+Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
+deprecated_syntax.lean:71:0-71:8: warning: syntax 'commandMyDepCmd' has been deprecated: use `#check` instead
+
+Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
+42 : Nat
+deprecated_syntax.lean:77:0-77:12: warning: macro 'commandMyWrapperCmd' produces deprecated syntax 'commandMyDepCmd': use `#check` instead
+
+Note: This linter can be disabled with `set_option linter.deprecated.syntax false`
+42 : Nat
+42 : Nat
+deprecated_syntax.lean:84:0-84:39: warning: `deprecated_syntax` should specify the date or library version at which the deprecation was introduced, using `(since := "...")`