Where should SlimCheck/QuickCheck be?

Stream: lean4

[Hanting Zhang]

Right now, mathlib4 has a version of QuickCheck ported from Haskell sitting in the Testing folder. I was looking for ways to generate random samples for some unit tests I'm writing. This is amazing and basically does everything I want already. The problem is that it's sitting in mathlib, so adding SlimCheck as a dependency would add the entirely of mathlib. We would rather not have this.

In general, testing is going to be useful everywhere, especially for non-math programming projects. I wonder if it would be desirable to move SlimCheck out of mathlib into its own thing, or perhaps into Lean4 core, etc.

cc @Henrik Böving What are your thoughts on this? Other opinions are welcome too!

[Henrik Böving]

The general idea right now is that mathlib4 in its current state is not supposed to be viewed the same way as mathlib in Lean 3. mathlib4 is basically a dumpster for everything that didn't fit into the compiler because we don't want to bother the compiler team with additional PRs that are not crucial to it. The idea was that at some point in the future :tm: we start ripping stuff out of mathlib4 into a real standard library (Std is not a standard library but "everything the compiler needs to bootstrap that doesnt fit in Init or Lean"). I'd say when that eventually happens we can look into phasing SlimCheck out into another library.

That being said i remember comitting to other mathlib files as well to get the termination proofs right so SlimCheck is actually not fully independent of mathlib4 as is right now, we'd end up reproducing lemmas if we were to rip it right now. For the current time you can just add mathlib4 as a dependency and we'll figure out the better solution when the current focus (the current focus being "get the mathlib working") is done.

[Henrik Böving]

I think that in general the quesiton as to which proofs and structures go into an stdlib and which go into future mathlib4 is a very interesting one. Having the eco system split up too much is not good for non computer scientists because things can get confusing and you suddenly end up having dependencies and stuff which isn't really something monorepo mathlib from Lean 3 had to deal with

[Hanting Zhang]

termination_by?! What are we here, mathematicians?! :laughing:
But thanks for the answers! Adding mathlib as a dependency isn't actually the end of the world. I agree SlimCheck would belong in the StdLib, but I guess we'll have to wait and see

[Hanting Zhang]

@Henrik Böving On some further thought, would it be possible to make a copy of the code? With the Apache copyright and credit to you, of course.

[Henrik Böving]

Sure apache allows that after all you don't have to ask me :p, but you'll also have to copy parts of matlhib etc. for the proofs