## Stream: general

### Topic: tiny stdlib between core and mathlib

#### Johan Commelin (May 11 2020 at 18:03):

After my experiments documented over at:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/moving.20algebra.20out.20of.20core
I'm wondering: should we carve out a well-designed and stable stdlib that sits between core and mathlib?
I can imagine that for a lot of CS applications, you don't want to have all of mathlib as a dependency. On the other hand, having maths locked into core is really annoying.

So maybe we can have some gcd(CS, math) in a stdlib, that involves nat, int, list, rbtree, and a bit more.

#### Johan Commelin (May 11 2020 at 18:03):

The benefit would be that it would still be relatively easy to change things, if necessary.

#### Kevin Buzzard (May 11 2020 at 18:03):

oh yeah that well-known mathematical object rbtree

#### Johan Commelin (May 11 2020 at 18:04):

Ok, maybe I shouldn't have said gcd(CS, math)

#### Kevin Buzzard (May 11 2020 at 18:05):

maybe you should have just told me it was a tree :-)

#### Jannis Limperg (May 11 2020 at 18:33):

Having three tightly coupled but formally independent projects imho sounds worse than having two. Counterproposal: Leave the 'general interest' stuff in core and move related code from mathlib to core. (Also, a well-designed and stable stdlib is a pretty large undertaking. The Agda standard library has 50k lines of code and many parts of it only became good after a few iterations.)

Counter-counterproposal: Wait for Lean 4 and don't spend too much time prettifying a soon-to-be-legacy codebase.

#### Reid Barton (May 11 2020 at 18:41):

I think Johan's proposal would be good for an ideal world but, in practice, we don't have any stable layer at all at this point.

#### Yury G. Kudryashov (May 11 2020 at 18:43):

+1 for counter-counterproposal.

#### Gabriel Ebner (May 11 2020 at 18:43):

For purely practical reasons, I think that until Lean 4 comes we're most productive moving as much as possible into mathlib.

#### Johan Commelin (May 11 2020 at 20:18):

For me that's completely fine. I still don't have a good idea of what lean is used for besides mathlib... we can always think about this idea if people start complaining that core has too little...

#### Kevin Buzzard (May 11 2020 at 22:06):

Do the people at Galois use it? @Simon Hudon do you know what goes on there? And do MS use Lean 3 for anything or are they all on Lean 4 now?

#### Simon Hudon (May 11 2020 at 22:08):

As far as I'm aware, the people at Galois are working with Lean 4. And all the 2 people at MS are using Lean 4 too

Who is Galois?

#### Jalex Stark (May 11 2020 at 22:29):

(Is it these people? It's hard to search for groups named galois... i literally typed galois group into google and was disappointed)

#### Reid Barton (May 11 2020 at 22:29):

https://galois.com/

#### Jalex Stark (May 11 2020 at 22:30):

thanks that makes a lot more sense

#### Simon Hudon (May 11 2020 at 22:30):

Galois is a R&D company doing a lot of formal methods work. They are known as a big user of Haskell and this is where I learned to use Lean

#### Mario Carneiro (May 12 2020 at 06:14):

I think that for the time being we should assume that any use of community lean 3 is going via mathlib. Even if most of mathlib is not a requirement, it can be trimmed down based on file inclusion for those that need to. But organizationally it's definitely easier to keep everything in one repo.

Last updated: May 08 2021 at 10:12 UTC