Distribution packaging

Stream: lean4

[Leah Neukirchen]

Hello, I'm working on packaging Lean 4 for Void Linux, and I wondered if a stage1 or stage2 build should be distributed, given the 4.0.0 tarball.

[Sebastian Ullrich]

Hi Leah, apologies in advance for not answering your actual question, but: we would really prefer distributions to package elan instead as even with monthly releases, the breaking nature of Lean releases makes it unlikely that distribution and project Lean version will be compatible in practice

[Leah Neukirchen]

so, do the elan packages use stage1 or stage2 builds? ;) I'm not sure which breakage you're expecting ? Or do you mean there will be many versions in use?

[Patrick Massot]

Yes, please don't try to package Lean directly. This would only cause users to hate you and we would be very sorry.

[Kevin Buzzard]

Lean updates every few weeks, projects contain metadata saying precisely which version of lean they use, and fixing one installation of lean means that now you can't use 99% of the projects because they use another version; there is no backwards compatibility so really these projects do not work with your fixed choice. elan is the Lean package manager and this is what every user needs in practice given the current state of the ecosystem.