Zulip Chat Archive

Stream: general

Topic: tiny stdlib between core and mathlib


view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 11 2020 at 18:03):

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

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:03):

oh yeah that well-known mathematical object rbtree

view this post on Zulip Johan Commelin (May 11 2020 at 18:04):

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

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:05):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 18:43):

+1 for counter-counterproposal.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 11 2020 at 22:27):

Who is Galois?

view this post on Zulip 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)

view this post on Zulip Reid Barton (May 11 2020 at 22:29):

https://galois.com/

view this post on Zulip Jalex Stark (May 11 2020 at 22:30):

thanks that makes a lot more sense

view this post on Zulip 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

view this post on Zulip 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: Sep 29 2021 at 00:36 UTC