Derive checkers (DecOpt instances) using new unification/schedule-based algorithm#30
Merged
ngernest merged 19 commits intometaprogrammingfrom Aug 8, 2025
Merged
Derive checkers (DecOpt instances) using new unification/schedule-based algorithm#30ngernest merged 19 commits intometaprogrammingfrom
DecOpt instances) using new unification/schedule-based algorithm#30ngernest merged 19 commits intometaprogrammingfrom
Conversation
…list relation in isRecCall)
…last element of the arg list is (some true))
DecOpt instances) using new unification/schedule-based algorithm
ngernest
added a commit
that referenced
this pull request
Aug 12, 2025
…ary` instances (#35) * chore: bump toolchain to v4.19.0 * chore: add #guard_msgs to noisy test * chore: add #guard_msgs to noisy test * chore: bump toolchain to v4.20.0-rc1 * chore: bump toolchain to v4.20.0-rc2 * chore: bump toolchain to v4.20.0 * chore: bump toolchain to v4.21.0-rc1 (#26) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.21.0-rc1 --------- Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump toolchain to v4.21.0-rc2 (#27) * chore: bump toolchain to v4.21.0-rc3 (#28) * chore: bump toolchain to v4.21.0 * chore: bump toolchain to v4.22.0-rc1 (#30) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc1 * chore: bump toolchain to v4.22.0-rc2 (#31) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc2 * chore: bump toolchain to v4.22.0-rc3 (#32) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc3 * chore: bump toolchain to v4.22.0-rc4 (#34) * patches for nightly-2025-01-04, and drop Batteries dependency * fix adaptation note * merge main * fixes for leanprover/lean4#7516 * merge lean-pr-testing-7516 * deprecations * chore: bump toolchain to v4.22.0-rc4 * Derive Arbitrary instances for algebraic data types * Only import linter from Batteries in Testable.lean * Specialize imports (avoid importing Lean directly) * Remove .DS_Store from .gitignore * Remove comment from Plausible.lean * Avoid thunking sub-generators * Update snapshot tests (sub-generators no longer thunked & are now explicitly parenthesized) * Remove mention of "simple inductive types" Co-authored-by: Kyle Miller <kmill31415@gmail.com> * Replace command elaborator with trace class * Update snapshot tests to use trace class instead of command elaborator * Update module docs following Kyle's suggestions * Remove deprecated command elaborator from nolints.json * Remove unused function * Rename ArbitrarySized to ArbitraryFueled following Eric's suggestion * Remove global constants in Idents file * Update snapshot tests to use size' + 1 instead of Nat.succ size' * Rename size function parameter in derived generators to fuel * Add counterexample property to Tree snapshot test * Add module docs for Tree snapshot test * Add counterexample property to Regular Expression snapshot test * Add counterexample property for STLC snapshot test * Add counterexample property for structure test * Fix typo in tests * Add counterexample property for Binop generator test * Add counterexample property for Value generator test * Remove unnecessary equality check for booleans * Add counterexample property for BitVec generator test * Emit error message when target type has no non-recursive constructors * Formatting in Random.lean * Refactor to use same logic as Deriving Repr (handle parameterized types + mutually inductive types) * Update snapshot tests * Add implicit parameters to derived generator for parameterized types * Update tests based on changes to accomodate parameterized types * Add docstrings to make linter happy * Handle mutually recursive types (need to add local let-definitions for Arbitrary instances) * Add snapshot test for mutually recursive types * Add counterexample property for mutually inductive type test * Improve shrinkers for trees * For parameterized types, ArbitraryFueled instances should have inst-implicit Arbitrary binders * Add counterexample property for parameterized type test * Remove Idents file, use Core.mkFreshUserName to produce fresh names instead * Remove mkLetBind (just create let-bind exprs directly using quotations) * Remove mkMatch combinators, just create match-exprs using quotations * Remove TSyntaxCombinators file, combinators are no longer used * Remove unnecessary if-condition * Refactor: move logic for setting ctorIsRecursive flag * Simplify logic for determining if constructors are recursive, remove Utils.lean * Remove spurious instance loop involving SampleableExt -> Arbitrary -> SampleableExt * Simplify logic for parenthesizing sub-generators * Loop fusion when computing sub-generator weights * Clean up nolints.json * Add newline * Replace all instances of LocalContext.getUnusedName w/ Core.mkFreshUserName * Remove mentions of Enum in README * Remove Enum mention * Remove linter & dependency on Batteries * Remove scripts/nolints.json * Fix typo in regular expression test docstring * Moving around definitions so that STLC tests compile * Remove duplicate Arbitrary file, move around definitions some more * Remove mentions of outdated command elaborator #derive_arbitrary in README --------- Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
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
1 participant
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.
This PR takes the improvements for deriving ArbitrarySuchThat instances from #27 , and applies them when deriving checkers (i.e.
DecOptinstances). See #27 for more details.At a high level, the algorithm for deriving checkers now uses the unification algorithm from Generating Good Generators and the mechanism for computing generator schedules from Testing Theorems.
Also in this PR:
DecOptinstances#deriving...commands have been use the new unification/schedule-based algorithm instead