Add Plausible integration (alternative to SlimCheck)

LSpec.lean

@@ -2,3 +2,4 @@ module
 public import LSpec.LSpec
 public import LSpec.Instances
 public import LSpec.SlimCheck
+public import LSpec.Plausible

LSpec/Plausible.lean

@@ -0,0 +1,170 @@
+module
+public meta import LSpec.LSpec
+public meta import Plausible
+
+/-!
+# Plausible integration for `LSpec`
+
+This module provides an alternative property-based testing backend for `LSpec`
+built on Lean's official [Plausible](https://github.com/leanprover-community/plausible)
+library.
+
+For backwards-compatibility reasons, the functions in this module live alongside LSpec's
+SlimCheck-based `check`/`checkIO`functions, as opposed to replacing them.
+
+The new entry points are:
+
+- **`checkPlausible`/`checkPlausible'`**: compile-time property tests
+- **`checkPlausibleIO`/`checkPlausibleIO'`**: runtime property tests with configurable seeds
+-/
+
+namespace LSpec
+public meta section
+
+/-- Variant of `Plausible.Testable.runSuiteAux`: tries `n` times to find a counter-example to `p`,
+    and reports the no. of trials that succeeded before a counterexample was found. -/
+def runPlausibleSuiteAux (p : Prop) [Plausible.Testable p] (cfg : Plausible.Configuration) :
+    Plausible.TestResult p → Nat → Plausible.Gen (Plausible.TestResult p × Nat)
+  | r, 0 => return (r, cfg.numInst)
+  | r, n + 1 => do
+    let size (_ : Nat) := (cfg.numInst - n - 1) * cfg.maxSize / cfg.numInst
+    let x ← Plausible.retry ((Plausible.Testable.runProp p cfg true).resize size) cfg.numRetries
+    match x with
+    | .success (PSum.inl ()) => runPlausibleSuiteAux p cfg x n
+    | .gaveUp g => runPlausibleSuiteAux p cfg (Plausible.giveUp g r) n
+    | _ => return (x, cfg.numInst - n - 1)
+
+/-- Variant of `Plausible.Testable.runSuite` (tries to find a counter-example to `p`),
+    but also tracks the no. of trials that succeeded before a counterexample was found. -/
+def runPlausibleSuite (p : Prop) [Plausible.Testable p] (cfg : Plausible.Configuration := {}) :
+    Plausible.Gen (Plausible.TestResult p × Nat) :=
+  runPlausibleSuiteAux p cfg (.gaveUp 0) cfg.numInst
+
+/-- Variant of `Plausible.Testable.checkIO` (run a test suite for `p` in `IO` using the global RNG
+    in `stdGenRef`), but also tracks the no. of trials that succeeded. -/
+def runPlausibleSuiteIO (p : Prop) [Plausible.Testable p] (cfg : Plausible.Configuration := {}) :
+    IO (Plausible.TestResult p × Nat) :=
+  match cfg.randomSeed with
+  | none => Plausible.Gen.run (runPlausibleSuite p cfg) 0
+  | some seed => Plausible.runRandWith seed (runPlausibleSuite p cfg)
+
+/-- Bridges a `Plausible.Testable` instance into LSpec's `Testable` result type,
+    running the suite at compile time with a fixed seed for deterministic results. -/
+abbrev instTestableOfPlausible (p : Prop) (cfg : Plausible.Configuration) [Plausible.Testable p] :
+    Testable p :=
+  match ReaderT.run (Plausible.runRandWith 0 (runPlausibleSuite p cfg)) ⟨0⟩ with
+  | .error _ => .isFailure 0 cfg.numInst "Generation failure"
+  | .ok (.success (.inr h), _) => .isTrue h
+  | .ok (.success (.inl _), _) => .isPassed cfg.numInst
+  | .ok (.gaveUp n, _) => .isFailure 0 cfg.numInst s!"Gave up {n} times"
+  | .ok (.failure h xs n, numSamples) =>
+    .isFalse h (numSamples + 1) cfg.numInst $ Plausible.Testable.formatFailure "Found problems!" xs n
+
+open Plausible.Decorations in
+/--
+Property-based test evaluated at compile time, using Plausible.
+
+This is the Plausible-based counterpart to `check`, which uses SlimCheck.
+Generates random test cases and checks the property during elaboration with a fixed random seed,
+making results deterministic across compilations.
+
+- `descr`: Description shown in test output (can be empty if propString is provided)
+- `p`: The property to check (e.g., `∀ n m : Nat, n + m = m + n`)
+- `next`: Next test in the sequence (default: `.done`)
+- `cfg`: Plausible configuration (number of tests, etc.)
+- `propString`: Optional string representation of the property for display
+
+```lean
+#lspec checkPlausible "addition commutes" (∀ n m : Nat, n + m = m + n)
+#lspec checkPlausible "with config" (∀ n : Nat, n + 0 = n) .done { numInst := 50 }
+```
+
+For runtime evaluation with configurable seeds, use `checkPlausibleIO` instead.
+-/
+def checkPlausible (descr : String) (p : Prop) (next : TestSeq := .done)
+    (cfg : Plausible.Configuration := {}) (propString : Option String := none)
+    (p' : DecorationsOf p := by mk_decorations) [Plausible.Testable p'] : TestSeq :=
+  haveI : Testable p' := instTestableOfPlausible p' cfg
+  .individual descr p' propString inferInstance next
+
+open Plausible.Decorations in
+/--
+Property-based test evaluated at runtime, using Plausible.
+
+This is the Plausible-based analog to `checkIO`. Unlike `checkPlausible`, which runs during
+compilation, `checkPlausibleIO` defers test execution until the test suite is run, enabling
+configurable random seeds via `cfg.randomSeed` and fresh random values on each run.
+
+- `descr`: Description shown in test output (can be empty if propString is provided)
+- `p`: The property to check (e.g., `∀ n m : Nat, n + m = m + n`)
+- `next`: Next test in the sequence (default: `.done`)
+- `cfg`: Plausible configuration including optional `randomSeed`
+- `propString`: Optional string representation of the property for display
+
+```lean
+def tests : TestSeq :=
+  checkPlausibleIO "addition commutes" (∀ n m : Nat, n + m = m + n)
+
+def reproducible : TestSeq :=
+  checkPlausibleIO "deterministic" (∀ n : Nat, n * 1 = n) .done { randomSeed := some 42 }
+
+def main : IO UInt32 := lspecIO (.ofList [("tests", [tests])]) []
+```
+
+Note: `checkPlausibleIO` tests are skipped when run via `#lspec` (which uses the pure runner).
+Use `lspecIO` or `lspecEachIO` to execute them.
+-/
+def checkPlausibleIO (descr : String) (p : Prop) (next : TestSeq := .done)
+    (cfg : Plausible.Configuration := {}) (propString : Option String := none)
+    (p' : DecorationsOf p := by mk_decorations) [Plausible.Testable p'] : TestSeq :=
+  let action : IO (Bool × Nat × Nat × Option String) := do
+    match ← runPlausibleSuiteIO p' cfg with
+    | (.success _, _) => pure (true, cfg.numInst, cfg.numInst, none)
+    | (.gaveUp n, _) => pure (false, 0, cfg.numInst, some s!"Gave up {n} times")
+    | (.failure _ xs n, numSamples) =>
+      pure (false, numSamples, cfg.numInst, some $ Plausible.Testable.formatFailure "Found problems!" xs n)
+  .individualIO descr propString action next
+
+section SyntaxCapturingMacros
+open Lean in
+/--
+Macro for `checkPlausible` that automatically captures the property syntax for display.
+
+This produces output like:
+```
+✓ ∃₁₀₀: "add_comm" (∀ n m : Nat, n + m = m + n)
+```
+
+Usage:
+```lean
+#lspec checkPlausible' "add_comm" (∀ n m : Nat, n + m = m + n)
+```
+-/
+scoped macro "checkPlausible'" descr:str prop:term : term => do
+  let propStr := prop.raw.reprint.getD s!"{prop}"
+  `((checkPlausible $descr $prop .done {} (some $(Lean.quote propStr)) : TestSeq))
+
+open Lean in
+/--
+Macro for `checkPlausibleIO` that automatically captures the property syntax for display.
+This is the Plausible counterpart to LSpec's `checkIO'` macro that currently uses SlimCheck.
+
+This produces output like:
+```
+✓ ∃₁₀₀: "add_comm" (∀ n m : Nat, n + m = m + n)
+```
+
+Usage:
+```lean
+def tests : TestSeq :=
+  checkPlausibleIO' "add_comm" (∀ n m : Nat, n + m = m + n)
+```
+-/
+scoped macro "checkPlausibleIO'" descr:str prop:term : term => do
+  let propStr := prop.raw.reprint.getD s!"{prop}"
+  `((checkPlausibleIO $descr $prop .done {} (some $(Lean.quote propStr)) : TestSeq))
+
+end SyntaxCapturingMacros
+
+end
+end LSpec

README.md

@@ -126,3 +126,74 @@ Once this is done a `Slimcheck` test is evaluated in a similar way to
 -- (0 shrinks)
 -- -------------------
 ```
+
+## Integration with `Plausible`
+
+LSpec also integrates with Lean's [Plausible](https://github.com/leanprover-community/plausible) property-based testing library. The Plausible backend lives alongside the SlimCheck-based `check`/`checkIO` 
+described above rather than replacing them, so existing SlimCheck tests continue to work unchanged.
+
+Plausible relies on the same core typeclasses as QuickCheck — `Shrinkable` and `SampleableExt`
+to generate and shrink random values — plus `Plausible.Testable` for the property itself.
+Instances for the common types (`Nat`, `Int`, `List`, etc.) ship with Plausible, and custom
+types are supported by providing `Shrinkable`/`SampleableExt` instances just as with SlimCheck.
+
+The module [LSpec.Plausible](LSpec/Plausible.lean) exposes two macros:
+
+* `checkPlausible'` — a **compile-time** property test, evaluated during elaboration with a
+  fixed random seed (deterministic across compilations). This is the Plausible-backed
+  counterpart to `check'`.
+* `checkPlausibleIO'` — a **runtime** property test, deferred until the test suite is run.
+  This enables fresh random values on each run and configurable seeds via `cfg.randomSeed`.
+  This is the Plausible-backed counterpart to `checkIO'`.
+
+Both macros capture the property syntax so it appears in the output. (Non-syntax-capturing
+`checkPlausible`/`checkPlausibleIO` functions are also available if you don't need the
+property echoed back.)
+
+A compile-time test with `#lspec`:
+
+```lean
+#lspec checkPlausible' "add_comm" (∀ n m : Nat, n + m = m + n)
+-- ✓ ∃₁₀₀: "add_comm" (∀ n m : Nat, n + m = m + n)
+
+#lspec checkPlausible' "bad" (∀ n : Nat, n < 5)
+-- × ∃¹⁰/₁₀₀: "bad" (∀ n : Nat, n < 5)
+
+-- ===================
+-- Found problems!
+-- n := 6
+-- issue: 6 < 5 does not hold
+-- (0 shrinks)
+-- -------------------
+```
+
+A runtime test, run via `lspecIO`. Because `checkPlausibleIO'` tests are skipped by the pure
+`#lspec` runner, they must be executed with `lspecIO` (or `lspecEachIO`):
+
+```lean
+open LSpec
+
+def plausibleTests : TestSeq :=
+  checkPlausibleIO' "add_comm" (∀ n m : Nat, n + m = m + n)
+
+def main : IO UInt32 := lspecIO (.ofList [("plausibleTests", [plausibleTests])]) []
+```
+
+Multiple property tests can be sequenced with `++`. Note that the `'`-suffixed macros
+capture everything up to the end of the line as the property, so to chain them use the
+non-capturing `checkPlausibleIO` function (which takes an explicit `next` argument):
+
+```lean
+def suite : TestSeq :=
+  checkPlausibleIO "add_comm" (∀ n m : Nat, n + m = m + n) $
+  checkPlausibleIO "mul_one"  (∀ n : Nat, n * 1 = n)
+```
+
+The `'`-suffixed macros always use the default configuration. To pass a fixed seed for
+reproducible runs (or otherwise customise the `Plausible.Configuration`), call the underlying
+`checkPlausibleIO` function directly:
+
+```lean
+def reproducible : TestSeq :=
+  checkPlausibleIO "add_comm" (∀ n m : Nat, n + m = m + n) .done { randomSeed := some 42 }
+```

Tests/Main.lean

@@ -147,6 +147,15 @@ def propertyTests : TestSeq :=
       (assertRunIO (checkIO "bad" (∀ n : Nat, n = n + 1)) false) .done
   )
 
+-- Variant of `propertyTests` above which tests the Plausible integration
+def plausiblePropertyTests : TestSeq :=
+  group "Plausible property tests" (
+    .individualIO "checkPlausibleIO passing property" none
+      (assertRunIO (checkPlausibleIO "add_zero" (∀ n : Nat, n + 0 = n)) true) .done ++
+    .individualIO "checkPlausibleIO failing property" none
+      (assertRunIO (checkPlausibleIO "bad" (∀ n : Nat, n = n + 1)) false) .done
+  )
+
 /-! ## lspecIO integration -/
 
 def lspecIOIntegration : TestSeq :=
@@ -233,6 +242,7 @@ def main (args : List String) : IO UInt32 := do
     ("Combinators", [combinatorTests]),
     ("Append", [appendTests]),
     ("Property tests", [propertyTests]),
+    ("Plausible property tests", [plausiblePropertyTests]),
     ("lspecIO integration", [lspecIOIntegration]),
     ("lspecEachIO", [lspecEachIOTests])
   ]

lake-manifest.json

@@ -1,5 +1,16 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "6304553",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
  "name": "LSpec",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lakefile.toml

@@ -3,6 +3,11 @@ version = "2.0.0"
 defaultTargets = ["LSpec"]
 testDriver = "tests"
 
+[[require]]
+name = "plausible"
+git = "https://github.com/leanprover-community/plausible"
+rev = "6304553"
+
 [[lean_lib]]
 name = "LSpec"