chore: deprecate := variants of inductive and structure

Deprecates `inductive ... :=` and `structure ... :=`. Currently this syntax produces a warning, controlled by the `linter.deprecated` option.

Part of leanprover#5236

Author: kmill

Diff for: src/Lean/Elab/Declaration.lean

@@ -136,8 +136,8 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
 /-
-leading_parser "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
-leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor >> optDeriving
+leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
+leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
 -/
 private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
   checkValidInductiveModifier modifiers
@@ -167,6 +167,12 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
   let classes ← liftCoreM <| getOptDerivingClasses decl[6]
+  if decl[3][0].isToken ":=" then
+    -- https://github.com/leanprover/lean4/issues/5236
+    if Linter.getLinterValue Linter.linter.deprecated (← getOptions) then
+      withRef decl[0] <| withRef decl[3] <| logWarning <| .tagged ``Linter.deprecatedAttr "\
+        'inductive ... :=' has been deprecated in favor of 'inductive ... where'.\n\
+        You can disable this warning with 'set_option linter.deprecated false'."
   return {
     ref             := decl
     shortDeclName   := name

Diff for: src/Lean/Elab/Structure.lean

@@ -137,7 +137,13 @@ def structSimpleBinder   := leading_parser atomic (declModifiers true >> ident)
 def structFields         := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 ```
 -/
-private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) :=
+private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) := do
+  if structStx[5][0].isToken ":=" then
+    -- https://github.com/leanprover/lean4/issues/5236
+    if Linter.getLinterValue Linter.linter.deprecated (← getOptions) then
+      withRef structStx[0] <| withRef structStx[5][0] <| logWarning <| .tagged ``Linter.deprecatedAttr "\
+        'structure ... :=' has been deprecated in favor of 'structure ... where'.\n\
+        You can disable this warning with 'set_option linter.deprecated false'."
   let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let mut fieldBinder := fieldBinder
@@ -866,7 +872,8 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
         addDefaults lctx defaultAuxDecls
 
 /-
-leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields >> optDeriving
+leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >>
+  optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving
 
 where
 def «extends» := leading_parser " extends " >> sepBy1 termParser ", "

Diff for: tests/lean/run/5236.lean

@@ -0,0 +1,20 @@
+/-!
+# Deprecate `:=` for `inductive` and `structure`
+-/
+
+/--
+warning: 'inductive ... :=' has been deprecated in favor of 'inductive ... where'.
+You can disable this warning with 'set_option linter.deprecated false'.
+-/
+#guard_msgs in
+inductive DogSound' :=
+  | woof
+  | grr
+
+/--
+warning: 'structure ... :=' has been deprecated in favor of 'structure ... where'.
+You can disable this warning with 'set_option linter.deprecated false'.
+-/
+#guard_msgs in
+structure S :=
+  (n : Nat)