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.
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
Website: https://lean-lang.org/ Also: https://leanprover-community.github.io/
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
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).
> 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.
(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.
(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.
I forgot to mention my copr repo: https://copr.fedorainfracloud.org/coprs/petersen/lean4/ though it doesn't have -2 yet
I suppose it might be better to install everything under /usr/lib64/lean/ at least until upstream wants to supports distro installation better.
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
Copr build: https://copr.fedorainfracloud.org/coprs/build/7449612 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/07449612-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2033719 [details] The .spec file difference from Copr build 7449612 to 7454612
Copr build: https://copr.fedorainfracloud.org/coprs/build/7454612 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/07454612-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2036608 [details] The .spec file difference from Copr build 7454612 to 7543712
Copr build: https://copr.fedorainfracloud.org/coprs/build/7543712 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/07543712-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2038925 [details] The .spec file difference from Copr build 7543712 to 7704052
Copr build: https://copr.fedorainfracloud.org/coprs/build/7704052 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/07704052-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2043322 [details] The .spec file difference from Copr build 7704052 to 7819198
Copr build: https://copr.fedorainfracloud.org/coprs/build/7819198 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/07819198-lean4/fedora-review/review.txt 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-libraries 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.
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.
(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
Posting the scratch build link first: https://koji.fedoraproject.org/koji/taskinfo?taskID=125509888 since running the testsuite will further the buildtime.
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
Created attachment 2055582 [details] The .spec file difference from Copr build 7819198 to 8209482
Copr build: https://copr.fedorainfracloud.org/coprs/build/8209482 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/08209482-lean4/fedora-review/review.txt 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-libraries 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.
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...
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
Created attachment 2059451 [details] The .spec file difference from Copr build 8209482 to 8305794
Copr build: https://copr.fedorainfracloud.org/coprs/build/8305794 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/08305794-lean4/fedora-review/review.txt 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-libraries 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.
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.
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?
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.
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(
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.
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.
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.
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
Created attachment 2060769 [details] The .spec file difference from Copr build 8305794 to 8332728
Copr build: https://copr.fedorainfracloud.org/coprs/build/8332728 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/08332728-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2065240 [details] The .spec file difference from Copr build 8332728 to 8492176
Copr build: https://copr.fedorainfracloud.org/coprs/build/8492176 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/08492176-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2075134 [details] The .spec file difference from Copr build 8492176 to 8606198
Copr build: https://copr.fedorainfracloud.org/coprs/build/8606198 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/08606198-lean4/fedora-review/review.txt 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-libraries 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.
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
Created attachment 2079113 [details] The .spec file difference from Copr build 8606198 to 8734417
Copr build: https://copr.fedorainfracloud.org/coprs/build/8734417 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/08734417-lean4/fedora-review/review.txt 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-libraries 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.
Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.20.0-3.fc43.src.rpm - requires for c++, gmp, and uv
Created attachment 2093774 [details] The .spec file difference from Copr build 8734417 to 9156407
Copr build: https://copr.fedorainfracloud.org/coprs/build/9156407 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/09156407-lean4/fedora-review/review.txt 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-libraries 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.
Spec URL: https://petersen.fedorapeople.org/reviews/lean4/lean4.spec SRPM URL: https://petersen.fedorapeople.org/reviews/lean4/lean4-4.20.0-4.fc43.src.rpm - require libstdc++-devel instead of gcc-c++ - fixup liblean_shared_1.so permissions (needed for c9s) - thanks @salimma
Created attachment 2093913 [details] The .spec file difference from Copr build 9156407 to 9160520
Copr build: https://copr.fedorainfracloud.org/coprs/build/9160520 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2277910-lean4/fedora-rawhide-x86_64/09160520-lean4/fedora-review/review.txt 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-libraries 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.