Requesting to move stuff from Mathlib into Batteries?

Stream: batteries

[Markus de Medeiros]

What is the process for moving stuff out of Mathlib and into Batteries?

I'm finding myself copy-pasting a bunch of stuff from Mathlib/Data/List/Nodup.lean just to work with the lemmas in Batteries/Data/List/Perm.lean, and it feels like these should be combined.

[cmlsharp]

I also have found myself wishing for Multiset in Batteries when e.g. doing the formal verification of BinaryHeap

[François G. Dorais]

To move stuff from Mathlib to Batteries, just make a PR: Create a new branch on your Batteries fork, copy the items you need from Mathlib. Adapt until it works, then contribute a PR to Batteries.

Things to keep in mind:

• As you fix imports, your PR will get larger and larger. Split it into logical pieces. While PRs can be too big, there is no such thing as a PR that is too small!
• There will need to be a companion Mathlib adaptation PR. Ask Kim for write access to Mathlib Testing so you can edit the batteries-pr-testing-nnnn branch and rely on CI to build Mathlib.

[Yury G. Kudryashov]

I'm not sure if our automation treats Mathlib Testing as a more priviledged fork. Is it bad for some reason to add it as a remote and make PRs to the corresponding batteries-pr-testing-nnnn?

[François G. Dorais]

AFAIK, Mathlib Testing is not privileged in the ecosystem. Besides, the testing branches don't make PRs to Mathlib Testing, they make PRs to Mathlib. The only difference is that Mathlib Testing branches still do CI when Mathlib would reject them because of irregular dependencies.

[Kim Morrison]

No, the nightly-testing fork is privileged, and only known community members should be given access to it.

[François G. Dorais]

It's in the Batteries README to ask for write access to Mathlib Nightly Testing but there are no instructions how to do that.

[Yury G. Kudryashov]

I think that we should change that. Instead, people should fork nightly testing and open a PR to the testing branch. Then a maintainer should merge that PR.

[Kim Morrison]

I'm happy to give write access there to people who are regularly helping maintain nightly-testing itself, but would prefer that we use PRs from forks for battery adaptations, despite the overhead.