Miscellaneous data structures in `Data`

Stream: mathlib4

[Michael Rothgang]

Going over the list of files in Data with autoImplicit on, I wonder if certain data structures are supposed to stay in mathlib medium-term --- respectively, if the mathlib implementation can already be deleted in favour of batteries or similar. (If so, I might leave those files alone.) More specifically,

• UnionFind: is this superseded by the batteries implementation now? @Mario Carneiro You even wrote another implement for lean4lean, right - do you know more?
• ByteArray: same question, @François G. Dorais You wrote the batteries implementation, if I understood correctly.
• Vector. IIRC @Shreyas Srinivas worked on adding this to batteries; can/should the mathlib version be removed already?
• the MLList and List/EditDistance folders: @Kim Morrison IIRC, you wanted to remove the former, right?

[Shreyas Srinivas]

The Mathlib Vectors are supposed to stay. There is a bit-rotting PR (mathlib4#13407) to namespace Mathlib's Vector by me. (bit-rotting in the sense that merge conflicts keep piling up).

[Shreyas Srinivas]

The batteries PR (batteries#793) is also just sitting in the PR queue, which can be merged independently of the above Mathlib PR.

[Shreyas Srinivas]

There are good reasons to keep both versions in their respective namespaces. They have different APIs based on the underlying data structure.

[Shreyas Srinivas]

update: mathlib4#13407 has been merged. Thanks to @Floris van Doorn As described in the PR description and discussed on the linked zulip thread, it was not possible to provide a deprecation alias for this, since that would defeat the whole purpose of the PR (to remove Vector from the global namespace when Mathlib is imported). Users of Mathlib's Vectorshould know that they can use Vector as usual after opening the Mathlib namespace

[François G. Dorais]

Re ByteArray this is batteries#836 which has some issues.

[Kim Morrison]

Michael Rothgang said:

• the MLList and List/EditDistance folders: @Kim Morrison IIRC, you wanted to remove the former, right?

Yes, getting rid of quite a bit of MLList from Mathlib is on my TODO list, but fairly far down!

[Kim Morrison]

There's the unfortunate situation that rw_search uses MLList internally. I haven't had any time to work on rw_search since starting at the FRO, and so it has never really become a viable product.

If no one is using it, we can just remove it (to another repo?) and then just remove MLList from Mathlib entirely.

If people are using it, I'd like to keep it (it was actually one of my first ever Lean projects back in 2018 or something, so I have a soft spot for it :-), and hope that one day someone will work on it and bring it up to its potential. :-)

[Mario Carneiro]

@Michael Rothgang UnionFind in lean4lean is based on the one in mathlib, and the one in batteries is based on the one in lean4lean. The original is outdated and can be removed I think

[Michael Rothgang]

Mario Carneiro said:

Michael Rothgang UnionFind in lean4lean is based on the one in mathlib, and the one in batteries is based on the one in lean4lean. The original is outdated and can be removed I think

Thanks for the context! I filed #14556 to remove it.