Add Plausible integration (alternative to SlimCheck) - #82
Merged
samuelburnham merged 3 commits intoJul 27, 2026
Conversation
Introduce LSpec/Plausible.lean providing checkPlausible / checkPlausible'
(compile-time) and checkPlausibleIO / checkPlausibleIO' (runtime), backed
by Lean's official Plausible library. These live alongside the existing
SlimCheck-based check/checkIO rather than replacing them, so existing code
is unaffected.
The harness (runPlausibleSuite{,Aux,IO}, instTestableOfPlausible) tracks the
number of trials that succeeded before a counterexample was found, and funnels
into the shared LSpec.Testable / TestSeq machinery for reporting.
Uses 'public meta import' / 'public meta section' to match Plausible's own
module-system markings (Gen.resize, TestResult.gaveUp, etc. are meta).
arthurpaulino
approved these changes
Jul 27, 2026
arthurpaulino
left a comment
arthurpaulino
left a comment
Member
There was a problem hiding this comment.
The patch looks fine to me. @samuelburnham wdyt?
samuelburnham
approved these changes
Jul 27, 2026
samuelburnham
left a comment
samuelburnham
left a comment
Member
There was a problem hiding this comment.
Looks great, LGTM! We can add automation later to update the LSpec and plausible versions in lockstep.
Contributor
Author
|
Great, thank you both! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hi! This PR is a follow-up to issue #81. This PR integrates Lean's Plausible property-based testing library with LSpec, so that users can use LSpec's test harnesses to test Plausible properties.
(For backwards compatibility reasons, this PR treats the Plausible integration as an addition to LSpec's existing SlimCheck integration, instead of replacing SlimCheck.)
The new code introduced in this PR is deliberately designed to be as similar as possible to the existing SlimCheck integration for consistency purposes. Here is how the existing SlimCheck functions map onto their Plausible-backed counterparts:
runPlausibleSuiteAuxSlimCheck.Checkable.runSuiteAuxrunPlausibleSuiteSlimCheck.Checkable.runSuiterunPlausibleSuiteIOSlimCheck.Checkable.checkIOinstTestableOfPlausibleinstTestableOfCheckablecheckPlausiblecheckcheckPlausibleIOcheckIOcheckPlausible'check'checkPlausibleIO'checkIO'Note: the dependency on Plausible in
lakefile.tomlhas a specific commit hash specified as therev, as the latest version of Plausible uses Lean 4.33, whereas LSpec currently uses 4.31.(Feel free to suggest ways to change this PR! I am currently using a fork of LSpec with Plausible for testing my own Lean projects anyway, and I figured this may be useful to other LSpec users.)