fix: improve the logging behavior of slim_check (#10393)

There was a bug in the tactic that meant it would always print "no goals to be solved".

This also promotes the code-generation from `IO` to `CoreM`, so that the output can be sent through the logging infrastructure rather than `IO.println`.
This is important, because tests are not allowed to be noisy, and we have no way to capture `IO` output.

Mathlib/Tactic/SlimCheck.lean

@@ -199,9 +199,9 @@ set_option trace.Meta.synthInstance true
   --   when_tracing `slim_check.instance   <| do
   --   { inst ← summarize_instance inst >>= pp,
   --     trace!"\n[testable instance]{format.indent inst 2}" },
-  let code ← unsafe evalExpr (IO PUnit) q(IO PUnit) e
+  let code ← unsafe evalExpr (CoreM PUnit) q(CoreM PUnit) e
   _ ← code
-  admitGoal (← getMainGoal)
+  admitGoal g
 
 -- Porting note: below is the remaining code from mathlib3 which supports the
 -- `trace.slim_check.instance` trace option, and which has not been ported.

Mathlib/Testing/SlimCheck/Testable.lean

@@ -550,11 +550,11 @@ end Decorations
 open Decorations in
 /-- Run a test suite for `p` and throw an exception if `p` does not hold. -/
 def Testable.check (p : Prop) (cfg : Configuration := {})
-    (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : IO PUnit := do
+    (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : Lean.CoreM PUnit := do
   match ← Testable.checkIO p' cfg with
-  | TestResult.success _ => if !cfg.quiet then IO.println "Success"
-  | TestResult.gaveUp n => if !cfg.quiet then IO.println s!"Gave up {n} times"
-  | TestResult.failure _ xs n => throw (IO.userError <| formatFailure "Found problems!" xs n)
+  | TestResult.success _ => if !cfg.quiet then Lean.logInfo "Success"
+  | TestResult.gaveUp n => if !cfg.quiet then Lean.logWarning s!"Gave up {n} times"
+  | TestResult.failure _ xs n => Lean.throwError <| formatFailure "Found problems!" xs n
 
 -- #eval Testable.check (∀ (x y z a : Nat) (h1 : 3 < x) (h2 : 3 < y), x - y = y - x)
 --   Configuration.verbose

test/slim_check.lean

@@ -3,6 +3,24 @@ import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Data.Finsupp.Notation
 import Mathlib.Testing.SlimCheck.Functions
 
+/--
+warning: Gave up 91 times
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (z : Nat) (h : z = 37) : z ≠ 0 := by
+  slim_check (config := { randomSeed := some 257 })
+
+/--
+info: Success
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (z : Nat) (h : z ≤ 37) : z ≤ 37 := by
+  slim_check (config := { randomSeed := some 257 })
+
 -- Porting note:
 -- These are the tests from mathlib3, updated to Lean 4 syntax.
 -- Many of these fail, I think because of missing `Testable` instances.