[Package]: Lean 4 - Githubissues

ooloh2Ai commented 1 month ago

Why is it worth to add this package?

It is a computer proof assistant, with which we could write up formal mathematical proofs.

Home page URL

https://lean-lang.org/

Source code URL

https://github.com/leanprover/lean4

Packaging policy acknowledgement

[X] The project is actively developed.
[X] The project has existing packages and is "well known".
[X] Licensed under an open source license.
[X] Not available through a language package manager: pip, npm, cpan, cargo, etc.
[ ] Not taking up too much disk space (< 100MiB per architecture, exceptions can be made)
[X] Not duplicating the functionality of existing packages.
[X] Not serving hacking, malware, phishing, spamming, spying, ddos functionality.
[X] I certify that I have read Termux Packaging Policy and understand that my request will be denied if it is found lacking.

Additional information

Somebody succeeded to compile it under Termux: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean.204.20installation.20on.20Android/near/478086727

Wait for them to comment.

kim-em commented 1 month ago

Lean developer here: please don't do this. Lean is intended to be used via elan, and package managers should not bundle a binary themselves. This will only ever result in a broken experience for users.

(Moreover, Lean is well over 100MiB.)

(Thank you, though, for a great product which I use regularly. :-)

TomJo2000 commented 1 month ago

Yeah I came pretty much to the same conclusion.

We'd need to disable elan as it wouldn't be compatible with Termux (unless upstream wants to start building releases for us I guess...)
The package is over our usual size guidelines, which can be waived but it's always a tradeoff for repo size and the mirrors.
Lean is mostly self hosted (e.g. written in Lean), which would likely entail a fairly complicated build process.

I'm afraid Termux just isn't a platform that's gonna fit for Lean. You might still be able to use it on Termux through a Proot environment ^{(i.e. proot-distro https://github.com/termux/proot-distro)} But I have neither tested nor validated that option, and it would entail some overhead from Proot.

In theory the package could be moved to the TUR, but the same packaging concerns would still apply.

ooloh2Ai commented 1 month ago

We'd need to disable elan as it wouldn't be compatible with Termux (unless upstream wants to start building releases for us I guess...)

Could you please explain a bit why elan would not be compatible with Termux? Is it possible to modify elan a bit so that it would work under Termux?