-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor: move slim_check to plausible #18459
base: master
Are you sure you want to change the base?
Conversation
85d4564
to
497cd3a
Compare
PR summary 27e644c811
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Tactic.SlimCheck | 442 | 0 | -442 (-100.00%) |
Mathlib.Testing.SlimCheck.Gen | 361 | 0 | -361 (-100.00%) |
Mathlib.Testing.SlimCheck.Sampleable | 440 | 0 | -440 (-100.00%) |
Mathlib.Testing.SlimCheck.Testable | 441 | 0 | -441 (-100.00%) |
Mathlib.Tactic | 2331 | 2322 | -9 (-0.39%) |
Import changes for all files
Files | Import difference |
---|---|
Mathlib.Testing.SlimCheck.Functions |
-697 |
Mathlib.Tactic.SlimCheck |
-442 |
Mathlib.Testing.SlimCheck.Testable |
-441 |
Mathlib.Testing.SlimCheck.Sampleable |
-440 |
Mathlib.Testing.SlimCheck.Gen |
-361 |
Mathlib.Tactic |
-9 |
Mathlib.Testing.Plausible.Testable |
57 |
Mathlib.Testing.Plausible.Sampleable |
413 |
Mathlib.Testing.Plausible.Functions |
685 |
Declarations diff
- And.printableProp
- Bool.printableProp
- Bool.sampleableExt
- Bool.shrinkable
- Char.sampleable
- Char.sampleableDefault
- Char.shrinkable
- Configuration
- DecorationsOf
- Eq.printableProp
- False.printableProp
- Fin.sampleableExt
- Fin.shrinkable
- Gen
- Gen.run
- Iff.printableProp
- Imp.printableProp
- Int.sampleableExt
- Int.shrinkable
- LE.printableProp
- LT.printableProp
- List.sampleableExt
- List.shrinkable
- List.toFinmap'
- MyType
- NamedBinder
- Nat.sampleableExt
- Nat.shrink
- Nat.shrinkable
- Ne.printableProp
- NoShrink
- Not.printableProp
- Or.printableProp
- Pi.sampleableExt
- PrintableProp
- Prod.sampleableExt
- Prod.shrinkable
- Prop.sampleableExt
- SampleableExt
- Shrinkable
- Sigma.shrinkable
- TestResult
- Testable
- Testable.check
- Testable.checkIO
- Testable.runSuite
- Testable.runSuiteAux
- TotalFunction
- TotalFunction.inhabited
- True.printableProp
- addInfo
- addShrinks
- addVarInfo
- and
- andTestable
- apply
- arrayOf
- choose
- chooseAny
- chooseNatLt
- chooseNatLt_aux
- combine
- comp
- decGuardTestable
- elements
- foo
- forallTypesTestable
- formatFailure
- get
- getSize
- giveUp
- iff
- iffTestable
- imp
- inhabited
- instance (priority := 2000) PiPred.sampleableExt [SampleableExt (α → Bool)] :
- instance (priority := 2000) PiUncurry.sampleableExt [SampleableExt (α × β → γ)] :
- instance (priority := 2000) subtypeVarTestable {p : α → Prop} {β : α → Prop}
- instance (priority := high) unusedVarTestable {β : Prop} [Nonempty α] [Testable β] :
- instance (priority := low) : PrintableProp p
- instance (priority := low) decidableTestable {p : Prop} [PrintableProp p] [Decidable p] :
- instance (α : Type u) (β : Type v) [Repr α] [Repr β] : Repr (TotalFunction α β)
- instance : SampleableExt MyType
- instance : Shrinkable MyType
- instance : ToExpr Configuration
- instance : ToString (TestResult p) := ⟨toString⟩
- instance {α : Type u} {m : Type u → Type*} [Pure m] : Inhabited (OptionT m α)
- interpSample
- isFailure
- listOf
- minimize
- mk
- mkGenerator
- mkSelfContained
- oneOf
- or
- orTestable
- permutationOf
- printSamples
- prodOf
- propVarTestable
- reprAux
- resize
- retry
- runProp
- sampleableExt
- shrink
- shrinkable
- slimTrace
- testBit_pred
- toString
- varTestable
- verbose
-- repr
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh
contains some details about this script.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
I think we should keep the |
b9fab57
to
27e644c
Compare
This moves Mathlib to the now pulled out (and already slightly improved)
version of slim_check at https://github.com/leanprover-community/plausible/.
I removed both all instances and logic as well as all tests that are already
covered by plausible itself and only left what Mathlib needs for itself.