https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Bug ID: 2277910 Summary: Review Request: lean4 - Functional programming language and theorem prover Product: Fedora Version: rawhide URL: https://lean-lang.org/ Status: NEW Component: Package Review Assignee: nobody@fedoraproject.org Reporter: petersen@redhat.com QA Contact: extras-qa@fedoraproject.org CC: package-review@lists.fedoraproject.org Target Milestone: --- Classification: Fedora
Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.7.0-1.fc41.src.rpm
Description: Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #1 from Jens Petersen petersen@redhat.com --- Koji scratch build: https://koji.fedoraproject.org/koji/taskinfo?taskID=117041038
To be transparent here is the rpmlint I see when submitting:
lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/globs/TBA.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/globs/TBA/Eulerian.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/globs/TBA/Eulerian/A.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/lock/Nop.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/noBuild/Test.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/order/A.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/order/A/B/C.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/order/bar/X.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/order/foo/X.lean lean4.x86_64: E: zero-length /usr/src/lean/lake/tests/precompileArgs/Foo/Bar.lean lean4.x86_64: W: unstripped-binary-or-object /usr/bin/lake lean4.x86_64: W: unstripped-binary-or-object /usr/bin/lean lean4.x86_64: W: unstripped-binary-or-object /usr/bin/leanc lean4.x86_64: W: unstripped-binary-or-object /usr/lib/lean/libInit_shared.so lean4.x86_64: W: unstripped-binary-or-object /usr/lib/lean/libleanshared.so lean4.x86_64: E: static-library-without-debuginfo /usr/lib/lean/libInit.a lean4.x86_64: E: static-library-without-debuginfo /usr/lib/lean/libLake.a lean4.x86_64: E: static-library-without-debuginfo /usr/lib/lean/libLean.a lean4.x86_64: E: static-library-without-debuginfo /usr/lib/lean/libleancpp.a lean4.x86_64: E: static-library-without-debuginfo /usr/lib/lean/libleanrt.a lean4.x86_64: E: spelling-error ('prover', 'Summary(en_US) prover -> prove, rover, proverb') lean4.x86_64: E: spelling-error ('prover', '%description -l en_US prover -> prove, rover, proverb') lean4.src: E: spelling-error ('prover', 'Summary(en_US) prover -> prove, rover, proverb') lean4.src: E: spelling-error ('prover', '%description -l en_US prover -> prove, rover, proverb') lean4.spec:31: E: rpm-buildroot-usage %build %cmake -DLEAN_BUILD_TYPE="Release" -DUSE_GITHASH=OFF -DLEAN_INSTALL_PREFIX=%{buildroot} lean4.spec:31: E: rpm-buildroot-usage %build %cmake -DLEAN_BUILD_TYPE="Release" -DUSE_GITHASH=OFF -DLEAN_INSTALL_PREFIX=%{buildroot} lean4.x86_64: W: no-manual-page-for-binary lake lean4.x86_64: W: no-manual-page-for-binary lean lean4.x86_64: W: no-manual-page-for-binary leanc lean4.x86_64: W: no-manual-page-for-binary leanmake lean4.x86_64: W: files-duplicate /usr/src/lean/lake/tests/clone/test/Main.lean /usr/src/lean/lake/tests/buildArgs/Main.lean lean4.x86_64: W: devel-file-in-non-devel-package /usr/include/lean/config.h lean4.x86_64: W: devel-file-in-non-devel-package /usr/include/lean/lean.h lean4.x86_64: W: devel-file-in-non-devel-package /usr/include/lean/lean_gmp.h lean4.x86_64: W: devel-file-in-non-devel-package /usr/include/lean/version.h lean4.x86_64: W: devel-file-in-non-devel-package /usr/lib/lean/libInit.a lean4.x86_64: W: devel-file-in-non-devel-package /usr/lib/lean/libLake.a lean4.x86_64: W: devel-file-in-non-devel-package /usr/lib/lean/libLean.a lean4.x86_64: W: devel-file-in-non-devel-package /usr/lib/lean/libleancpp.a lean4.x86_64: W: devel-file-in-non-devel-package /usr/lib/lean/libleanrt.a 2 packages and 1 specfiles checked; 21 errors, 19 warnings, 10 filtered, 21 badness; has taken 6.6 s
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #2 from Jens Petersen petersen@redhat.com --- Website: https://lean-lang.org/
Also: https://leanprover-community.github.io/
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #3 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.7.0-2.fc41.src.rpm
strip bin and lib*.so files
Koji scratch build: https://koji.fedoraproject.org/koji/taskinfo?taskID=117065121
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Fabio Valentini decathorpe@gmail.com changed:
What |Removed |Added ---------------------------------------------------------------------------- CC| |decathorpe@gmail.com
--- Comment #4 from Fabio Valentini decathorpe@gmail.com --- Sorry, I'm slightly confused why you think stripping the binaries manually is necessary? This will break debuginfo generation built-in to RPM (and indeed you defined %debug_package to %nil to fix that).
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #6 from Jens Petersen petersen@redhat.com --- (In reply to Fabio Valentini from comment #4)
Sorry, I'm slightly confused why you think stripping the binaries manually is necessary? This will break debuginfo generation built-in to RPM (and indeed you defined %debug_package to %nil to fix that).
Well no debuginfo seems generated, but that might be fixable perhaps. Note that lean4 is written in lean4, so I am not sure that it is fixable. Though the bootstrap is via C++. That's my rough understanding anyway.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #7 from Jens Petersen petersen@redhat.com --- (In reply to Fabio Valentini from comment #5)
lean4.spec:31: E: rpm-buildroot-usage %build %cmake -DLEAN_BUILD_TYPE="Release" -DUSE_GITHASH=OFF -DLEAN_INSTALL_PREFIX=%{buildroot} lean4.spec:31: E: rpm-buildroot-usage %build %cmake -DLEAN_BUILD_TYPE="Release" -DUSE_GITHASH=OFF -DLEAN_INSTALL_PREFIX=%{buildroot}
Also, I'm not sure whether the `%buildroot` macro is actually defined in %build.
I could retest but this was the only way I could get it to build: not the prettiest I certainly agree.
https://github.com/leanprover/lean4/issues/3068 is the upstream issue I had opened to get to this point.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #8 from Jens Petersen petersen@redhat.com --- I forgot to mention my copr repo: https://copr.fedorainfracloud.org/coprs/petersen/lean4/ though it doesn't have -2 yet
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #9 from Jens Petersen petersen@redhat.com --- I suppose it might be better to install everything under /usr/lib64/lean/ at least until upstream wants to supports distro installation better.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #10 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.7.0-3.fc41.src.rpm
install under libdir/lean4 for now with symlinks to bindir
Koji scratch build: https://koji.fedoraproject.org/koji/taskinfo?taskID=117737138
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #11 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/7449612 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Does not provide -static: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #12 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.7.0-4.fc41.src.rpm
link with -lgmp instead of libgmp.so file
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #13 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2033719 --> https://bugzilla.redhat.com/attachment.cgi?id=2033719&action=edit The .spec file difference from Copr build 7449612 to 7454612
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #14 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/7454612 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Does not provide -static: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #15 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.8.0-1.fc41.src.rpm
- https://lean-lang.org/blog/2024-6-1-lean-480/ - https://github.com/leanprover/lean4/releases/tag/v4.8.0
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #16 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2036608 --> https://bugzilla.redhat.com/attachment.cgi?id=2036608&action=edit The .spec file difference from Copr build 7454612 to 7543712
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #17 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/7543712 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Does not provide -static: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Benson Muite benson_muite@emailplus.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Flags| |fedora-review? Assignee|nobody@fedoraproject.org |benson_muite@emailplus.org CC| |benson_muite@emailplus.org
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #18 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.9.0-1.fc41.src.rpm
- https://lean-lang.org/blog/2024-7-1-lean-490/ - https://github.com/leanprover/lean4/releases/tag/v4.9.0
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #19 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2038925 --> https://bugzilla.redhat.com/attachment.cgi?id=2038925&action=edit The .spec file difference from Copr build 7543712 to 7704052
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #20 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/7704052 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #21 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.10.0-1.fc41.src.rpm
- https://github.com/leanprover/lean4/releases/tag/v4.10.0 - add some macros to handle minor point releases
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #22 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2043322 --> https://bugzilla.redhat.com/attachment.cgi?id=2043322&action=edit The .spec file difference from Copr build 7704052 to 7819198
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #23 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/7819198 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #24 from Benson Muite benson_muite@emailplus.org --- It seems preferable to do a stage2 or stage3 build: https://lean-lang.org/lean4/doc/dev/bootstrap.html
Probably also helpful to run some of the tests. Ctest should work, see: https://github.com/leanprover/lean4/blob/master/.github/workflows/ci.yml
May need to add libuv and ccache as dependencies.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #25 from Jens Petersen petersen@redhat.com --- (In reply to Benson Muite from comment #24)
It seems preferable to do a stage2 or stage3 build: https://lean-lang.org/lean4/doc/dev/bootstrap.html
I am not sure: we are not really doing a pure bootstrap in Fedora, upstream keeps the bootstrap files (stage0) up to date automatically merging in changes from stage1, so I don't believe stage 2 is actually required downstream in Fedora.
I checked the upstream release builds and nearly all of the them don't use stage 2 or 3. (There is one job which does but it is "Linux" and not "Linux Release". See for example the latest v4.13.0 release:
https://github.com/leanprover/lean4/actions/runs/11622555613
Probably also helpful to run some of the tests. Ctest should work, see: https://github.com/leanprover/lean4/blob/master/.github/workflows/ci.yml
May need to add libuv and ccache as dependencies.
Okay I am adding ctest, thanks
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #26 from Jens Petersen petersen@redhat.com --- Posting the scratch build link first: https://koji.fedoraproject.org/koji/taskinfo?taskID=125509888 since running the testsuite will further the buildtime.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #27 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.13.0-1.fc42.src.rpm
update to 4.13 and enable ctest
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #28 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2055582 --> https://bugzilla.redhat.com/attachment.cgi?id=2055582&action=edit The .spec file difference from Copr build 7819198 to 8209482
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #29 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/8209482 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/lean_libuv.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #30 from Jens Petersen petersen@redhat.com --- Having now tested my package a bit: I am finding one problem with libuv, which is giving constant gcc linker warnings when building projects:
$ lake build : ℹ [9/27] Replayed Curl.Errors:c.o info: stderr: gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done ℹ [10/27] Replayed Curl.CurlM:c.o info: stderr: gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done ℹ [11/27] Replayed Curl.HeaderData:c.o info: stderr: gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done ℹ [17/27] Replayed Main:c.o info: stderr: gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done :
while not fatal, it's very noisy and annoying.
Need to work out what is causing that: the official upstream toolchain does not have this issue...
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #31 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.13.0-4.fc42.src.rpm
- use sed to override GMP_LIBRARIES and LIBUV_LIBRARIES with pkgconf --libs
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #32 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2059451 --> https://bugzilla.redhat.com/attachment.cgi?id=2059451&action=edit The .spec file difference from Copr build 8209482 to 8305794
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #33 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/8305794 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/lean_libuv.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Sebastian Ullrich sebastian@lean-fro.org changed:
What |Removed |Added ---------------------------------------------------------------------------- CC| |sebastian@lean-fro.org
--- Comment #34 from Sebastian Ullrich sebastian@lean-fro.org --- As a Lean maintainer, I need to point out that while it is of course within your right to package this software, our official stance is to heavily discourage doing so. Lean features monthly releases with no backwards-compatibility guarantees. Thus installing any fixed version of Lean is almost guaranteed to lead to misery about mismatched version expectations in downloaded projects, which we then have to debug and explain when users invariably complain. Packaging the Lean version manager https://github.com/leanprover/elan instead is a strictly more favorable option for everyone involved.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #35 from Benson Muite benson_muite@emailplus.org --- To distribute any software that builds using Lean in Fedora, the Lean toolchain needs to be packaged. It is possible to automate the updates using Packit, see https://packit.dev/ - which may also be helpful in checking that updates to Lean build on Fedora. It is understandable that there will be breaking changes. Certainly elan can also be packaged for people to build Lean applications on their own machines. Is the expectation that software programmed in Lean will only be used by software developers, or will there be expectations that non-programmers may find it useful to have verifiable programs?
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #36 from Sebastian Ullrich sebastian@lean-fro.org --- Verified software is being written in Lean, but it will probably take quite a bit more time for this to extend to projects end users may want to install using their distro package manager. And similar to Rust etc., it will likely need a separate discussion on how to best do that first. I assume this review request was not submitted with the intention of building other packages either. So for now, without specific Lean-based software that wants to be packaged in mind, we only gain to confuse direct users of Lean by packaging a single fixed version. I should also add that Mathlib, Lean's most widely-used library, currently targets Lean prereleases, so Fedora users of this package would be guaranteed to use a Lean version incompatible with it. At the very least, such a package should not be included before elan is, to avoid at least some of the confusion.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #37 from Jens Petersen petersen@redhat.com --- Well if lean4 lands in Fedora Linux - my intention would be to update it monthly to the latest release. Perhaps Fedora Rawhide (development) could even track the rc's. We also have arch's in Fedora not supported upstream.
Though I have also been toying with the thought to have versioned builds (eg lean4.13) in my Copr repo. [1] Though my impression is projects/packages are encouraged or hoped to keep up with releases as best they can? Im theory we could also have versioned lean4 packages in Fedora too. I feel for small projects and learning just having the current stable version available in Fedora is still useful for some people.
I assume this review request was not submitted with the intention of building other packages either.
Well that is the long-term intention yes, though currently nothing particular in mind yet, but I would like to eventually. I think of lean4 also as a potential possible modern replacement for Haskell: it's a beautiful language. Though my impression is the current lean4 (lake) library package story may not be well suited to binary packages? In Fedora Rust, packages are now only shipped as source crates - perhaps a similar model might work for lean4.
I am not sure if packaging mathlib in Fedora makes sense currently or in the future - in theory the stable version tags could be built I suppose. I may try to experiment with library packaging some time in the future.
I agree it would be good to have elan packaged in Fedora too, though I am not really a Rust packager. I have a quick and dirty package in copr too [2] and I am using it personally with my lean4 rpm package (using "elan toolchain link").
[1] https://copr.fedorainfracloud.org/coprs/petersen/lean4/ [2] https://copr.fedorainfracloud.org/coprs/petersen/elan/
Anyway I don't seem to be making myself too popular, upstream ;o(
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Benson Muite benson_muite@emailplus.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Flags| |needinfo?(sebastian@lean-fr | |o.org)
--- Comment #38 from Benson Muite benson_muite@emailplus.org --- 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.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
Sebastian Ullrich sebastian@lean-fro.org changed:
What |Removed |Added ---------------------------------------------------------------------------- Flags|needinfo?(sebastian@lean-fr | |o.org) |
--- Comment #39 from Sebastian Ullrich sebastian@lean-fro.org --- I have nothing further to add here. I think you make some good points, they may just be a few years too early in Lean's FOSS packaging timeline.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #40 from Jens Petersen petersen@redhat.com --- One idea I wanted to add/propose (for the fast moving versions - since lean4 is on a monthly release cadence, ie somewhat faster than rust): Long ago I did versioned subpackaging of ghc (compare with the current ghcX.Y coverage) - ie there was a main ghc package providing also ghcX.Y.Z subpackages which for better or worse would persist (remain) installed after a ghc version update.
Probably some would argue reasonably that this would be unreasonable - though just occurred to me a further workaround could be to add an optional/recommended obsoletes subpackage to remove older subpkg versions.
But I feel this could work reasonably well for lean4 with its fast cadence - addressing the upstream concerns about multi-version support.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #41 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.14.0-1.fc42.src.rpm
- update to 4.14
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #42 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2060769 --> https://bugzilla.redhat.com/attachment.cgi?id=2060769&action=edit The .spec file difference from Copr build 8305794 to 8332728
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #43 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/8332728 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/lean_libuv.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #44 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.15.0-1.fc42.src.rpm
update to 4.15
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #45 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2065240 --> https://bugzilla.redhat.com/attachment.cgi?id=2065240&action=edit The .spec file difference from Copr build 8332728 to 8492176
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #46 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/8492176 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/lean_libuv.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #47 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.16.0-1.fc42.src.rpm
- https://github.com/leanprover/lean4/releases/tag/v4.16.0
Koji scratch build: https://koji.fedoraproject.org/koji/taskinfo?taskID=128837469
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #48 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2075134 --> https://bugzilla.redhat.com/attachment.cgi?id=2075134&action=edit The .spec file difference from Copr build 8492176 to 8606198
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #49 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/8606198 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/lean_libuv.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #50 from Jens Petersen petersen@redhat.com --- Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.17.0-1.fc42.src.rpm
- https://github.com/leanprover/lean4/releases/tag/v4.17.0
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #51 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Created attachment 2079113 --> https://bugzilla.redhat.com/attachment.cgi?id=2079113&action=edit The .spec file difference from Copr build 8606198 to 8734417
https://bugzilla.redhat.com/show_bug.cgi?id=2277910
--- Comment #52 from Fedora Review Service fedora-review-bot@fedoraproject.org --- Copr build: https://copr.fedorainfracloud.org/coprs/build/8734417 (succeeded)
Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-rev...
Found issues:
- lean4 : /usr/lib64/lean4/include/lean/config.h lean4 : /usr/lib64/lean4/include/lean/lean.h lean4 : /usr/lib64/lean4/include/lean/lean_gmp.h lean4 : /usr/lib64/lean4/include/lean/lean_libuv.h lean4 : /usr/lib64/lean4/include/lean/version.h Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#_devel_packages - Package has .a files: lean4. Illegal package name: lean4. Read more: https://docs.fedoraproject.org/en-US/packaging-guidelines/#packaging-static-...
Please know that there can be false-positives.
--- This comment was created by the fedora-review-service https://github.com/FrostyX/fedora-review-service
If you want to trigger a new Copr build, add a comment containing new Spec and SRPM URLs or [fedora-review-service-build] string.
package-review@lists.fedoraproject.org