who will maintain batteries?

Stream: batteries

[Bulhwi Cha]

Mario Carneiro and Kim Morrison both seem too busy to review pull requests for Batteries. Besides, the Lean FRO doesn't have to maintain it because it's one of the Lean community's libraries. Then who will do the work?

[Bulhwi Cha]

If no one would review these stale PRs, would it be advisable to move the part that Mathlib depends on from Batteries to Mathlib?

[Kim Morrison]

If there are PRs that result in functional differences to Mathlib, please let me know about them here and I will make time to review them!

[Kim Morrison]

(But yes, I have not otherwise been finding time to review the PR list at Batteries.)

[Yaël Dillies]

Is it on the table to elongate the list of batteries maintainers?

[Ruben Van de Velde]

Is there much left in scope for batteries now that core is absorbing so much?

[Kim Morrison]

Very sorry for the lack of news here, trying to coordinate messaging on the mathlib maintainers list. I have two thumbs up and no objections about posting the following, so I'll start with this:

The future of batteries is still under discussion. (My understanding is that at present progress is blocked on scheduling a meeting amongst the mathlib maintainers, which is difficult as many academics are just starting a new semester.)

In the meantime, may I suggest as alternatives:

• New work could possibly live in stand-alone repositories.
• Material containing solely missing theorems about "basic" data types List / Array / UIntX / BitVec etc. can be discussed with Kim Morrison for inclusion in the Lean standard library.
• As usual, mathematical theory should go to Mathlib.

[Bulhwi Cha]

Ruben Van de Velde said:

Is there much left in scope for batteries now that core is absorbing so much?

Maybe Batteries can have tactics that the FRO doesn't want to include in Lean's core and standard libraries.

[François G. Dorais]

I'm not a Mathlib maintainer. Is there a way to be notified when the said meeting would occur and possibly listen to it? A recording would be fine but a back-seat listen-in with no option to chime-in would be fine as well.

Kim Morrison said:

Very sorry for the lack of news here, trying to coordinate messaging on the mathlib maintainers list. I have two thumbs up and no objections about posting the following, so I'll start with this:

The future of batteries is still under discussion. (My understanding is that at present progress is blocked on scheduling a meeting amongst the mathlib maintainers, which is difficult as many academics are just starting a new semester.)

In the meantime, may I suggest as alternatives:

• New work could possibly live in stand-alone repositories.
• Material containing solely missing theorems about "basic" data types List / Array / UIntX / BitVec etc. can be discussed with Kim Morrison for inclusion in the Lean standard library.
• As usual, mathematical theory should go to Mathlib.
  

[François G. Dorais]

François G. Dorais said:

I'm not a Mathlib maintainer. Is there a way to be notified when the said meeting would occur and possibly listen to it? A recording would be fine but a back-seat listen-in with no option to chime-in would be fine as well.

Full disclosure: I was invited to the meeting but I couldn't make it. Nevertheless, the meeting went well and I am personally pleased with the outcome. There will be more Batteries news soon...