Zulip Chat Archive

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

Jalex Stark (May 11 2020 at 22:27):

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: Dec 20 2023 at 11:08 UTC