https://bugzilla.redhat.com/show_bug.cgi?id=2277910 Benson Muite <benson_muite@xxxxxxxxxxxxx> changed: What |Removed |Added ---------------------------------------------------------------------------- Flags| |needinfo?(sebastian@lean-fr | |o.org) --- Comment #38 from Benson Muite <benson_muite@xxxxxxxxxxxxx> --- It is helpful to have the early version of the compiler for people to try out, as well as to test building software with. Usually, many compilers become completely self-hosting, so without early versions, bootstraping can become a chore. Rust is great for hyperscalers who want to move fast, but has one disadvantage - software built using rust typically has many dependencies for which it is difficult to follow vulnerabilities. The sharing of code for C/C++ programs usually results in more people checking the stable code releases. Long lived API and ABI compatibility make code maintenance easier - if one needs to do an expensive code audit, then the hope is that the audited code can be used for some period of time, and any needed fixes can be backported. If someone needs a new feature that is not yet stable, they can build the software from source. Many people are aware of the reproducibility crisis in scientific work that uses software where rather than checking that the correct functionality is obtained, one checks that by using the exact same set of dependencies specified by particular commits of software dependencies, the same numerical result is obtained. Hopefully Lean4 will not share such a fate. The Python ecosystem is an example of one where after significant effort the infrastructure aligns well with what is on PyPI. Will there be something similar for Lean4? We do like a human in the loop check of what is included in Fedora. We also like to ensure the entire system works well together so elan while great for developers should not be the only solution.Indicating which version of mathlib corresponds to the current release version of the Lean4 compiler would be a good first step to enabling inclusion in Linux distributions. Your thesis mentions enabling portability for Linux by distributing an old glibc: https://lean-lang.org/papers/thesis-sebastian.pdf This is enabled by careful software engineering practices that do not cause most programs to break when glibc is updated. Building Lean4 in Fedora would enable good testing of this. In particular, one may want to integrate Lean4 with other software that needs features in a newer glibc version or uses the Lean4 FFI: https://lean-lang.org/lean4/doc/dev/ffi.html It may also help when people use musl, GNU Herd, BSD etc. See for example: https://www.freshports.org/math/lean4/ To summarize, it is understandable that Lean4 may have breaking changes, new programming languages take some time to stabilize, so shielding early bleeding edge users by using elan is helpful. However, it would be good to support other workflows. -- You are receiving this mail because: You are always notified about changes to this product and component You are on the CC list for the bug. https://bugzilla.redhat.com/show_bug.cgi?id=2277910 Report this comment as SPAM: https://bugzilla.redhat.com/enter_bug.cgi?product=Bugzilla&format=report-spam&short_desc=Report%20of%20Bug%202277910%23c38 -- _______________________________________________ package-review mailing list -- package-review@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to package-review-leave@xxxxxxxxxxxxxxxxxxxxxxx Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/package-review@xxxxxxxxxxxxxxxxxxxxxxx Do not reply to spam, report it: https://pagure.io/fedora-infrastructure/new_issue
