fix: give TestResult.success (.inl ()) higher priority than .gaveUp

Plausible/Testable.lean

@@ -518,10 +518,8 @@ def retry (cmd : Gen (TestResult p)) : Nat → Gen (TestResult p)
 
 /-- Count the number of times the test procedure gave up. -/
 def giveUp (x : Nat) : TestResult p → TestResult p
-  | success (PSum.inl ()) => gaveUp x
-  | success (PSum.inr p) => success <| (PSum.inr p)
   | gaveUp n => gaveUp <| n + x
-  | TestResult.failure h xs n => failure h xs n
+  | r => r
 
 /-- Try `n` times to find a counter-example for `p`. -/
 def Testable.runSuiteAux (p : Prop) [Testable p] (cfg : Configuration) :
@@ -534,13 +532,13 @@ def Testable.runSuiteAux (p : Prop) [Testable p] (cfg : Configuration) :
       slimTrace s!"Retrying up to {cfg.numRetries} times until guards hold"
     let x ← retry ((Testable.runProp p cfg true).resize size) cfg.numRetries
     match x with
-    | success (PSum.inl ()) => runSuiteAux p cfg r n
+    | success (PSum.inl ()) => runSuiteAux p cfg x n
     | gaveUp g => runSuiteAux p cfg (giveUp g r) n
     | _ => return x
 
 /-- Try to find a counter-example of `p`. -/
 def Testable.runSuite (p : Prop) [Testable p] (cfg : Configuration := {}) : Gen (TestResult p) :=
-  Testable.runSuiteAux p cfg (success <| PSum.inl ()) cfg.numInst
+  Testable.runSuiteAux p cfg (gaveUp 0) cfg.numInst
 
 /-- Run a test suite for `p` in `IO` using the global RNG in `stdGenRef`. -/
 def Testable.checkIO (p : Prop) [Testable p] (cfg : Configuration := {}) : IO (TestResult p) :=

Test/Tactic.lean

@@ -159,3 +159,13 @@ theorem ulift_nat (f : ULift.{1} Nat) : f = ⟨0⟩ := by
 #guard_msgs in
 theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
   plausible (config := {quiet := true})
+
+-- https://github.com/leanprover-community/plausible/issues/15
+/--
+info: Unable to find a counter-example
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+theorem true_example_with_guard (a : Nat) (ha : 4 ≤ a) : a = a := by
+  plausible

Test/Testable.lean

@@ -24,6 +24,6 @@ instance : Arbitrary MyType :=
     let xyDiff ← SampleableExt.interpSample Nat
     return ⟨x, x + xyDiff, by omega⟩⟩
 
--- TODO: this is a noisy test.
--- We can't use `#guard_msgs` because the number of attempts to non-deterministic.
+/-- info: Unable to find a counter-example -/
+#guard_msgs in
 #eval Testable.check <| ∀ a b : MyType, a.y ≤ b.x → a.x ≤ b.y