mathlib vs std

Stream: lean4

[Bhakti Shah]

Kind of curious, is there a reason there's lemmas split between Mathlib.a.b.c and Std.a.b.c? For example Mathlib.Data.List.Basic and Std.Data.List.Basic. Not really an actual issue but it's a bit counterintuitive + makes imports a lil confusing. Is it just to make the std library lighter?

[Yury G. Kudryashov]

In Lean 3, we moved almost everything to mathlib.

[Yury G. Kudryashov]

Now we're gradually moving stuff that doesn't need definitely-non-std stuff like docs#Monoid to Std.

[Bhakti Shah]

is this going to be breaking changes? or will you maintain two copies, one in Std and one in Mathlib? (or is this process written up somewhere ig)

[Scott Morrison]

This is going to be breaking changes.

[Yury G. Kudryashov]

Why is it breaking? Mathlib.Data.List.Basic imports Std.Data.List.Basic, so if your code imported Mathlib.Data.List.Basic, then moving a lemma to Std doesn't break your code.

[Yury G. Kudryashov]

But sometimes we change API while moving (e.g., this happens a lot to Fin defs and lemmas).