feat: unnecessary termination_by clauses cause warnings, not errors (#4809)

fixes #4804

Author: nomeata

src/Lean/Elab/PreDefinition/Main.lean

@@ -114,7 +114,7 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
       if !structural && !preDefsWithout.isEmpty then
         let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
         let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
-        logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++
+        logErrorAt termBy.ref (m!"incomplete set of `termination_by` annotations:\n"++
           m!"This function is mutually with {m}, which {doOrDoes} not have " ++
           m!"a `termination_by` clause.\n" ++
           m!"The present clause is ignored.")

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -57,18 +57,18 @@ structure TerminationHints where
 
 def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
 
-/-- Logs warnings when the `TerminationHints` are present.  -/
+/-- Logs warnings when the `TerminationHints` are unexpectedly present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit := do
   match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
   | .none, .none, .none => pure ()
   | .none, .none, .some dec_by =>
-    logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
+    logWarningAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
   | .some term_by?, .none, .none =>
-    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
+    logWarningAt term_by? m!"unused `termination_by?`, function is {reason}"
   | .none, .some term_by, .none =>
-    logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
+    logWarningAt term_by.ref m!"unused `termination_by`, function is {reason}"
   | _, _, _ =>
-    logErrorAt hints.ref m!"unused termination hints, function is {reason}"
+    logWarningAt hints.ref m!"unused termination hints, function is {reason}"
 
 /-- True if any form of termination hint is present. -/
 def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=

tests/lean/termination_by.lean.expected.out

@@ -1,20 +1,20 @@
-termination_by.lean:9:2-9:18: error: unused `termination_by`, function is not recursive
-termination_by.lean:12:2-12:21: error: unused `decreasing_by`, function is not recursive
-termination_by.lean:15:2-16:21: error: unused termination hints, function is not recursive
-termination_by.lean:19:2-19:18: error: unused `termination_by`, function is partial
-termination_by.lean:22:2-22:21: error: unused `decreasing_by`, function is partial
-termination_by.lean:25:2-26:21: error: unused termination hints, function is partial
-termination_by.lean:29:0-29:16: error: unused `termination_by`, function is unsafe
-termination_by.lean:32:2-32:21: error: unused `decreasing_by`, function is unsafe
-termination_by.lean:35:2-36:21: error: unused termination hints, function is unsafe
-termination_by.lean:40:4-40:20: error: unused `termination_by`, function is not recursive
-termination_by.lean:44:4-44:20: error: unused `termination_by`, function is not recursive
-termination_by.lean:54:2-54:18: error: unused `termination_by`, function is not recursive
-termination_by.lean:62:2-62:23: error: Incomplete set of `termination_by` annotations:
+termination_by.lean:9:2-9:18: warning: unused `termination_by`, function is not recursive
+termination_by.lean:12:2-12:21: warning: unused `decreasing_by`, function is not recursive
+termination_by.lean:15:2-16:21: warning: unused termination hints, function is not recursive
+termination_by.lean:19:2-19:18: warning: unused `termination_by`, function is partial
+termination_by.lean:22:2-22:21: warning: unused `decreasing_by`, function is partial
+termination_by.lean:25:2-26:21: warning: unused termination hints, function is partial
+termination_by.lean:29:0-29:16: warning: unused `termination_by`, function is unsafe
+termination_by.lean:32:2-32:21: warning: unused `decreasing_by`, function is unsafe
+termination_by.lean:35:2-36:21: warning: unused termination hints, function is unsafe
+termination_by.lean:40:4-40:20: warning: unused `termination_by`, function is not recursive
+termination_by.lean:44:4-44:20: warning: unused `termination_by`, function is not recursive
+termination_by.lean:54:2-54:18: warning: unused `termination_by`, function is not recursive
+termination_by.lean:62:2-62:23: error: incomplete set of `termination_by` annotations:
 This function is mutually with isOdd, which does not have a `termination_by` clause.
 The present clause is ignored.
 Try this: termination_by x1 => x1
-termination_by.lean:79:2-79:27: error: Incomplete set of `termination_by` annotations:
+termination_by.lean:79:2-79:27: error: incomplete set of `termination_by` annotations:
 This function is mutually with Test.f, Test.h and Test.i, which do not have a `termination_by` clause.
 The present clause is ignored.
 termination_by.lean:101:2-101:27: error: Invalid `termination_by`; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`.