tiny stdlib between core and mathlib

Stream: general

[Johan Commelin]

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]

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

[Kevin Buzzard]

oh yeah that well-known mathematical object rbtree

[Johan Commelin]

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

[Kevin Buzzard]

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

[Jannis Limperg]

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]

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]

+1 for counter-counterproposal.

[Gabriel Ebner]

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

[Johan Commelin]

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]

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]

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

[Jalex Stark]

Who is Galois?

[Jalex Stark]

(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]

https://galois.com/

[Jalex Stark]

thanks that makes a lot more sense

[Simon Hudon]

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]

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.