From cdd982a030b13c2585d52312f80da8eb32e02553 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Wed, 1 Apr 2026 11:51:59 +0100 Subject: [PATCH] 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 --- src/Lean/Elab/BuiltinCommand.lean | 12 +++ src/Lean/Elab/Command.lean | 2 + src/Lean/Elab/DeprecatedSyntax.lean | 71 ++++++++++++++++ src/Lean/Elab/Quotation/Precheck.lean | 9 ++ src/Lean/Elab/Tactic/Basic.lean | 2 + src/Lean/Elab/Tactic/Grind/Config.lean | 2 + src/Lean/Elab/Term/TermElabM.lean | 2 + src/Lean/Parser/Command.lean | 9 ++ stage0/src/stdlib_flags.h | 2 +- tests/elab/deprecated_syntax.lean | 84 +++++++++++++++++++ .../elab/deprecated_syntax.lean.out.expected | 32 +++++++ 11 files changed, 226 insertions(+), 1 deletion(-) create mode 100644 src/Lean/Elab/DeprecatedSyntax.lean create mode 100644 tests/elab/deprecated_syntax.lean create mode 100644 tests/elab/deprecated_syntax.lean.out.expected diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index ed7cd6d3bc..44a5dac01b 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/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 diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 1b9bd26385..6289592f03 100644 --- a/src/Lean/Elab/Command.lean +++ b/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?) => diff --git a/src/Lean/Elab/DeprecatedSyntax.lean b/src/Lean/Elab/DeprecatedSyntax.lean new file mode 100644 index 0000000000..fcf138552e --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index 65e4ce97ec..ba0c42f0bd 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 8c3f1c62b5..413587b646 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind/Config.lean b/src/Lean/Elab/Tactic/Grind/Config.lean index 77284d85bb..6d1ca45c2f 100644 --- a/src/Lean/Elab/Tactic/Grind/Config.lean +++ b/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 diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index d33ff9cf32..0cfdb29f7b 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/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?) => diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 1a15110689..3ba6345d98 100644 --- a/src/Lean/Parser/Command.lean +++ b/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" /-- diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..b4202aa74a 100644 --- a/stage0/src/stdlib_flags.h +++ b/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 diff --git a/tests/elab/deprecated_syntax.lean b/tests/elab/deprecated_syntax.lean new file mode 100644 index 0000000000..cc4604b587 --- /dev/null +++ b/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 diff --git a/tests/elab/deprecated_syntax.lean.out.expected b/tests/elab/deprecated_syntax.lean.out.expected new file mode 100644 index 0000000000..07f8998f65 --- /dev/null +++ b/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 := "...")`