chore: deprecate := variants of inductive and structure (#5542)

Deprecates `inductive ... :=`, `structure ... :=`, and `class ... :=` in
favor of the `... where` variant. Currently this syntax produces a
warning, controlled by the `linter.deprecated` option.

Breaking change: modifies `Lean.Linter.logLintIf` to use
`Lean.Linter.getLinterValue` to determine if a linter value is set. This
means that the `linter.all` option now is taken into account when the
linter option is not set.

Part of #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,10 @@ 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
+    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
   return {
     ref             := decl
     shortDeclName   := name

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

@@ -137,7 +137,12 @@ 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
+    let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
+    withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[5][0]
+      s!"{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'."
   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
@@ -879,7 +884,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: src/Lean/Linter/Basic.lean

@@ -23,8 +23,14 @@ def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
   let disable := m!"note: this linter can be disabled with `set_option {linterOption.name} false`"
   logWarningAt stx (.tagged linterOption.name m!"{msg}\n{disable}")
 
-/-- If `linterOption` is true, print a linter warning message at the position determined by `stx`.
+/--
+If `linterOption` is enabled, print a linter warning message at the position determined by `stx`.
+
+Whether a linter option is enabled or not is determined by the following sequence:
+1. If it is set, then the value determines whether or not it is enabled.
+2. Otherwise, if `linter.all` is set, then its value determines whether or not the option is enabled.
+3. Otherwise, the default value determines whether or not it is enabled.
 -/
 def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
-  if linterOption.get (← getOptions) then logLint linterOption stx msg
+  if getLinterValue linterOption (← getOptions) then logLint linterOption stx msg

Diff for: tests/lean/linterMissingDocs.lean

@@ -53,7 +53,7 @@ structure Foo where
   {mk4 mk5 : Nat}
   [mk6 mk7 : Nat]
 
-class Bar (α : Prop) := mk ::
+class Bar (α : Prop) where mk ::
   (foo bar := 1)
 
 class Bar2 (α : Prop) where

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

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