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.