fix: make #check_failure's output be info (leanprover#6685)

This PR fixes the issue that `#check_failure`'s output is warning Closes leanprover#6684
opencompl · Jan 21, 2025 · e57245c · e57245c
1 parent 1311246
commit e57245c
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 2 deletions.
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
@@ -294,7 +294,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     modify fun s => { s with messages := {} };
     pure messages
   let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do
-    modify fun s => { s with messages := prevMessages ++ s.messages.errorsToWarnings }
+    modify fun s => { s with messages := prevMessages ++ s.messages.errorsToInfos }
   let prevMessages ← resetMessages
   let succeeded ← try
     x

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
@@ -448,6 +448,9 @@ def markAllReported (log : MessageLog) : MessageLog :=
 def errorsToWarnings (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
 
+def errorsToInfos (log : MessageLog) : MessageLog :=
+  { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.information } | _ => m) }
+
 def getInfoMessages (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
 

diff --git a/tests/lean/run/autoLift.lean b/tests/lean/run/autoLift.lean
@@ -19,7 +19,7 @@ set_option autoLift false
 
 set_option pp.mvars false in
 /--
-warning: type mismatch
+info: type mismatch
   f
 has type
   IO Nat : Type