Spec URL: https://jjames.fedorapeople.org/rocq-stdlib/rocq-stdlib.spec SRPM URL: https://jjames.fedorapeople.org/rocq-stdlib/rocq-stdlib-9.1.0-1.fc45.src.rpm Fedora Account System Username: jjames Description: Rocq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. This package includes the Rocq Standard Library, that is to say, the set of modules usually bound to the Stdlib.* namespace. Test builds for (and using) this package have been done in a COPR: https://copr.fedorainfracloud.org/coprs/jjames/Rocq9/builds/. I am willing to swap reviews.
Copr build: https://copr.fedorainfracloud.org/coprs/build/10205107 (failed) Build log: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2445874-rocq-stdlib/fedora-rawhide-x86_64/10205107-rocq-stdlib/builder-live.log.gz Please make sure the package builds successfully at least for Fedora Rawhide. - If the build failed for unrelated reasons (e.g. temporary network unavailability), please ignore it. - If the build failed because of missing BuildRequires, please make sure they are listed in the "Depends On" field --- 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.
APPROVED. Issues found: The spec has no %check section. The packager explained that tests are run as part of the main rocq build rather than in this package. rpmlint reports a zero-length file: /usr/lib64/ocaml/rocq-stdlib/META. This is not a blocker, but the packager should confirm whether this is intentional. rpmlint reports incorrect-fsf-address in /usr/share/licenses/rocq-stdlib/LICENSE. This is minor and should be fixed upstream if possible. Legend: [x] = Pass, [!] = Fail, [-] = Not applicable, [?] = Not evaluated ===== MUST items ===== Generic: [x]: Package successfully compiles and builds into binary rpms on at least one supported primary architecture. Reviewer comment: Package built successfully in COPR. [x]: Package is licensed with an open-source compatible license and meets other legal requirements as defined in the legal section of Packaging Guidelines. Reviewer comment: Nothing in the review output suggests non-free content in the packaged result. [x]: License field in the package spec file matches the actual license. Reviewer comment: License reviewed manually. Although licensecheck reports many unknown/generated files in the expanded source tree, the packaged content was evaluated and the License field is acceptable. [x]: License file installed when any subpackage combination is installed. [x]: %build honors applicable compiler flags or justifies otherwise. [x]: Package contains no bundled libraries or specifies bundled libraries with Provides: bundled(<libname>) if unbundling is not possible. [x]: Changelog in prescribed format. [x]: Sources contain only permissible code or content. [-]: Package contains desktop file if it is a GUI application. [-]: Development files must be in a -devel package [x]: Package uses nothing in %doc for runtime. [x]: Package consistently uses macros (instead of hard-coded directory names). [x]: Package is named according to the Package Naming Guidelines. [x]: Package does not generate any conflict. [x]: Package obeys FHS, except libexecdir and /usr/target. [x]: If the package is a rename of another package, proper Obsoletes and Provides are present. [x]: Requires correct, justified where necessary. Reviewer comment: Generated Requires/Provides look sane in the template output. [x]: Spec file is legible and written in American English. [x]: Package contains systemd file(s) if in need. [x]: Useful -debuginfo package or justification otherwise. [x]: Package is not known to require an ExcludeArch tag. [x]: Large documentation must go in a -doc subpackage. Large could be size (~1MB) or number of files. [x]: Package complies to the Packaging Guidelines [x]: Package installs properly. [x]: Rpmlint is run on all rpms the build produces. [x]: If (and only if) the source package includes the text of the license(s) in its own file, then that file, containing the text of the license(s) for the package is included in %license. [x]: The License field must be a valid SPDX expression. [x]: Package requires other packages for directories it uses. [x]: Package must own all directories that it creates. [x]: Package does not own files or directories owned by other packages. [x]: Package uses either %{buildroot} or $RPM_BUILD_ROOT [x]: Package does not run rm -rf %{buildroot} (or $RPM_BUILD_ROOT) at the beginning of %install. [x]: Macros in Summary, %description expandable at SRPM build time. [x]: Dist tag is present. [x]: Package does not contain duplicates in %files. [x]: Permissions on files are set properly. [x]: Package must not depend on deprecated() packages. [x]: Package use %makeinstall only when make install DESTDIR=... doesn't work. [x]: Package is named using only allowed ASCII characters. [x]: Package does not use a name that already exists. [x]: Package is not relocatable. [x]: Sources used to build the package match the upstream source, as provided in the spec URL. [x]: Spec file name must match the spec package %{name}, in the format %{name}.spec. [x]: File names are valid UTF-8. [x]: Packages must not store files under /srv, /opt or /usr/local ===== SHOULD items ===== Generic: [x]: Reviewer should test that the package builds in mock. Reviewer comment: Package built successfully in COPR. [-]: If the source package does not include license text(s) as a separate file from upstream, the packager SHOULD query upstream to include it. [x]: Final provides and requires are sane (see attachments). [?]: Package functions as described. [?]: Latest version is packaged. [x]: Package does not include license text files separate from upstream. [?]: Sources are verified with gpgverify first in %prep if upstream publishes signatures. Reviewer comment: gpgverify is not used. [?]: Package should compile and build into binary rpms on all supported architectures. [!]: %check is present and all tests pass. Reviewer comment: The spec has no %check section. The packager explained that tests are run as part of the main rocq build rather than in this package. [?]: Packages should try to preserve timestamps of original installed files. [x]: Buildroot is not present [x]: Package has no %clean section with rm -rf %{buildroot} (or $RPM_BUILD_ROOT) [x]: No file requires outside of /etc, /bin, /sbin, /usr/bin, /usr/sbin. [x]: Fully versioned dependency in subpackages if applicable. [x]: Packager, Vendor, PreReq, Copyright tags should not be in spec file [x]: Sources can be downloaded from URI in Source: tag [x]: SourceX is a working URL. [x]: Spec use %global instead of %define unless justified. ===== EXTRA items ===== Generic: [x]: Rpmlint is run on all installed packages. Note: No rpmlint messages. [x]: Large data in /usr/share should live in a noarch subpackage if package is arched. Rpmlint Checking: rocq-stdlib-9.1.0-1.fc45.x86_64.rpm rocq-stdlib-source-9.1.0-1.fc45.x86_64.rpm rocq-stdlib-9.1.0-1.fc45.src.rpm ============================ rpmlint session starts ============================ rpmlint: 2.8.0 configuration: /usr/lib/python3.14/site-packages/rpmlint/configdefaults.toml /etc/xdg/rpmlint/fedora-spdx-licenses.toml /etc/xdg/rpmlint/fedora.toml /etc/xdg/rpmlint/scoring.toml /etc/xdg/rpmlint/users-groups.toml /etc/xdg/rpmlint/warn-on-functions.toml rpmlintrc: [PosixPath('/tmp/tmp01kj6w0s')] checks: 32, packages: 3 rocq-stdlib.x86_64: E: zero-length /usr/lib64/ocaml/rocq-stdlib/META rocq-stdlib-source.x86_64: W: no-documentation rocq-stdlib.spec: W: no-%check-section rocq-stdlib.x86_64: E: incorrect-fsf-address /usr/share/licenses/rocq-stdlib/LICENSE 3 packages and 0 specfiles checked; 2 errors, 2 warnings, 13 filtered, 2 badness; has taken 3.2 s Rpmlint (installed packages) (none): E: there is no installed rpm "rocq-stdlib-source". ============================ rpmlint session starts ============================ rpmlint: 2.8.0 configuration: /usr/lib/python3.14/site-packages/rpmlint/configdefaults.toml /etc/xdg/rpmlint/fedora-spdx-licenses.toml /etc/xdg/rpmlint/fedora.toml /etc/xdg/rpmlint/scoring.toml /etc/xdg/rpmlint/users-groups.toml /etc/xdg/rpmlint/warn-on-functions.toml checks: 32, packages: 2 0 packages and 0 specfiles checked; 0 errors, 0 warnings, 0 filtered, 0 badness; has taken 0.0 s (none): E: there is no installed rpm "rocq-stdlib". There are no files to process nor additional arguments. Nothing to do, aborting. Source checksums https://github.com/rocq-prover/stdlib/archive/V9.1.0/rocq-stdlib-9.1.0.tar.gz : CHECKSUM(SHA256) this package : 2d66421c52ed32719a15cb039c368e063c4d85f670e3d142f5eb7415fb427985 CHECKSUM(SHA256) upstream package : 2d66421c52ed32719a15cb039c368e063c4d85f670e3d142f5eb7415fb427985 Requires rocq-stdlib (rpmlib, GLIBC filtered): rocq-core(x86-64) rocq-stdlib-source (rpmlib, GLIBC filtered): rocq-stdlib(x86-64) Provides rocq-stdlib: rocq-stdlib rocq-stdlib(x86-64) rocq-stdlib-source: rocq-stdlib-source rocq-stdlib-source(x86-64) Generated by fedora-review 0.11.0 (05c5b26) last change: 2025-11-29 Command line :/bin/fedora-review --no-colors --prebuilt --rpm-spec --name rocq-stdlib --mock-config /var/lib/copr-rpmbuild/results/configs/child.cfg Buildroot used: fedora-rawhide-x86_64 Active plugins: Shell-api, Generic Disabled plugins: PHP, R, Perl, Haskell, Python, Java, SugarActivity, fonts, C/C++, Ocaml Disabled flags: EXARCH, EPEL6, EPEL7, DISTTAG, BATCH
Thank you very much for the review! The empty META file is probably not needed. I will try removing it and see if anything breaks. I will notify upstream about the FSF address. Let me know the next time you need a review.
The Pagure repository was created at https://src.fedoraproject.org/rpms/rocq-stdlib
FEDORA-2026-0fa104ac88 (flocq-4.2.2-1.fc44, frama-c-32.1-2.fc44, and 9 more) has been submitted as an update to Fedora 44. https://bodhi.fedoraproject.org/updates/FEDORA-2026-0fa104ac88
FEDORA-2026-0fa104ac88 has been pushed to the Fedora 44 testing repository. Soon you'll be able to install the update with the following command: `sudo dnf upgrade --enablerepo=updates-testing --refresh --advisory=FEDORA-2026-0fa104ac88` You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2026-0fa104ac88 See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.
FEDORA-2026-0fa104ac88 (flocq-4.2.2-1.fc44, frama-c-32.1-2.fc44, and 9 more) has been pushed to the Fedora 44 stable repository. If problem still persists, please make note of it in this bug report.