Spec URL: https://jjames.fedorapeople.org/rocq/rocq.spec SRPM URL: https://jjames.fedorapeople.org/rocq/rocq-9.1.1-1.fc45.src.rpm Fedora Account System Username: jjames Description: This is a rename request. The current package name is coq. 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. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching. 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/10205104 (succeeded) Review template: https://download.copr.fedorainfracloud.org/results/@fedora-review/fedora-review-2445873-rocq/fedora-rawhide-x86_64/10205104-rocq/fedora-review/review.txt Please take a look if any issues were found. --- 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.
I'll review it
Ok, fedora-review took ~6 hours to make an automated review on my machine. This is long! Lots of rpmlint messages some of them are worth to address in the meantime. Considering this is mostly a rename I am not going to insist of handling them right now so here is my formal Package Review ============== Legend: [x] = Pass, [!] = Fail, [-] = Not applicable, [?] = Not evaluated [ ] = Manual review needed ===== MUST items ===== C/C++: [x]: Package does not contain kernel modules. [x]: Development (unversioned) .so files in -devel subpackage, if present. Note: Unversioned so-files in private %_libdir subdirectory (see attachment). Verify they are not in ld path. [x]: Package does not contain any libtool archives (.la) [x]: Package contains no static executables. [x]: Rpath absent or only used for internal libs. Generic: [x]: Package is licensed with an open-source compatible license and meets other legal requirements as defined in the legal section of Packaging Guidelines. [x]: License field in the package spec file matches the actual license. [x]: License file installed when any subpackage combination is installed. [X]: If the package is under multiple licenses, the licensing breakdown must be documented in the spec. [X]: Package requires other packages for directories it uses. Note: No known owner of /usr/lib64/ocaml/rocq- runtime/plugins/tutorial, /usr/lib64/ocaml/rocq-runtime/plugins [x]: Package owns all directories that it creates. [x]: Package does not own files or directories owned by other packages. [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. [x]: Development files stored 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]: The package is a rename of another package, and proper Obsoletes and Provides are present. [x]: Requires correct, justified where necessary. [x]: Spec file is legible and written in American English. [-]: Package does not contain systemd file(s). [x]: Useful -debuginfo package or justification otherwise. [x]: Package is not known to require an ExcludeArch tag (it technically does as other Ocaml packages). [x]: Package complies to the Packaging Guidelines [x]: Package successfully compiles and builds into binary rpms on at least one supported primary architecture. [x]: Package installs properly. [x]: Rpmlint is run on all rpms the build produces. Note: There are rpmlint messages (see attachment). [x]: The License field must be a valid SPDX expression. [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]: Package contains desktop file if it is a GUI application. [x]: Package installs a %{name}.desktop using desktop-file-install or desktop-file-validate if there is such a file. [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]: Large documentation must go in a -doc subpackage. Large could be size (~1MB) or number of files. Note: Documentation size is 7254 bytes in 2 files. [x]: Packages must not store files under /srv, /opt or /usr/local ===== SHOULD items ===== Generic: [-]: Uses parallel make %{?_smp_mflags} macro. [x]: Avoid bundling fonts in non-fonts packages. [-]: 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). [x]: Fully versioned dependency in subpackages if applicable. [?]: I did not test if the package functions as described. [x]: Latest version is packaged (9.1.1). [x]: Package does not include license text files separate from upstream. [x]: Patches link to upstream bugs/comments/lists or are otherwise justified. [-]: Sources weren't verified with gpgverify first in %prep. Note: gpgverify is not used. [+/- ]: %check is present but disabled. [x]: Packages should try to preserve timestamps of original installed files. [x]: Reviewer should test that the package builds in mock. [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]: 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]: Package should compile and build into binary rpms on all supported architectures. [x]: Spec use %global instead of %define unless justified. ===== EXTRA items ===== Generic: [x]: Rpmlint is run on debuginfo package(s). Note: No rpmlint messages. [x]: Rpmlint is run on all installed packages. Note: There are rpmlint messages (see attachment). [x]: Large data in /usr/share should live in a noarch subpackage if package is arched. [x]: Spec file according to URL is the same as in SRPM. Rpmlint ------- Checking: rocq-9.1.1-1.fc45.x86_64.rpm rocq-runtime-9.1.1-1.fc45.x86_64.rpm rocq-runtime-devel-9.1.1-1.fc45.x86_64.rpm rocq-core-9.1.1-1.fc45.x86_64.rpm rocq-core-source-9.1.1-1.fc45.x86_64.rpm coq-core-compat-9.1.1-1.fc45.x86_64.rpm rocq-coqide-server-9.1.1-1.fc45.x86_64.rpm rocq-coqide-server-devel-9.1.1-1.fc45.x86_64.rpm rocq-rocqide-9.1.1-1.fc45.x86_64.rpm rocq-doc-9.1.1-1.fc45.noarch.rpm rocq-9.1.1-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/tmpyyle7_d2')] checks: 32, packages: 11 rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Array/ArrayAxioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Array/PrimArray.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/BinNums/IntDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/BinNums/NatDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/BinNums/PosDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/CMorphisms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/CRelationClasses.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Equivalence.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Init.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Morphisms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Morphisms_Prop.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/RelationClasses.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/SetoidTactics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Coq818.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Coq819.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Coq820.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Rocq90.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/FloatAxioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/FloatClass.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/FloatOps.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/PrimFloat.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/SpecFloat.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Byte.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Datatypes.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Decimal.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Hexadecimal.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Logic.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Ltac.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Nat.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Notations.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Number.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Peano.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Prelude.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Specif.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Sumbool.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Tactics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Tauto.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Wf.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Lists/ListDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/BinNums.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/CarryType.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/PrimInt63.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Basics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Tactics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Utils.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Wf.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Relations/Relation_Definitions.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Setoids/Setoid.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Strings/PrimString.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Strings/PrimStringAxioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/derive/Derive.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/extraction/ExtrHaskellBasic.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/extraction/ExtrOcamlBasic.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/extraction/Extraction.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrbool.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrclasses.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssreflect.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrfun.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrsetoid.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrunder.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssrmatching/ssrmatching.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Array.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Bool.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Char.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq818.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq819.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Constant.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Constr.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Constructor.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Control.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Env.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Evar.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/FMap.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/FSet.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Float.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Fresh.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ident.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ind.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Init.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Int.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Lazy.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/List.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1CompatNotations.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac2.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Message.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Meta.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Notations.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Option.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Pattern.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Printf.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Proj.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Pstring.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/RedFlags.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ref.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Rewrite.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Std.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/String.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/TransparentState.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Uint63.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Unification.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/rocq-core/META rocq-rocqide.x86_64: E: zero-length /usr/lib64/ocaml/rocqide/META rocq-runtime.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/revision rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/btauto/g_btauto.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/cc/g_congruence.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/derive/g_derive.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/ltac/g_eqdecide.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/ltac/profile_ltac_tactics.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/nsatz/g_nsatz.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/rtauto/g_rtauto.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/zify/g_zify.mli rocq-runtime-devel.x86_64: E: static-library-without-debuginfo /usr/lib64/ocaml/rocq-runtime/vm/coqrun.a coq-core-compat.x86_64: E: spelling-error ('Rocq', '%description -l en_US Rocq -> Rock, Rococo') rocq.src: E: spelling-error ('homotopy', '%description -l en_US homotopy -> photocopy') rocq.x86_64: E: spelling-error ('homotopy', '%description -l en_US homotopy -> photocopy') rocq-runtime.x86_64: E: spelling-error ('prover', '%description -l en_US prover -> prove, rover, proverb') rocq-doc.noarch: W: python-sphinx-doctrees-leftover /usr/share/doc/rocq/refman-html/.doctrees coq-core-compat.x86_64: W: no-manual-page-for-binary coqpp coq-core-compat.x86_64: W: no-manual-page-for-binary coqtop.byte coq-core-compat.x86_64: W: no-manual-page-for-binary coqworkmgr rocq-coqide-server.x86_64: W: no-manual-page-for-binary coqidetop rocq-runtime.x86_64: W: no-manual-page-for-binary csdpcert rocq-runtime.x86_64: W: no-manual-page-for-binary ocamllibdep rocq-runtime.x86_64: W: no-manual-page-for-binary rocq.byte rocq-runtime.x86_64: W: no-manual-page-for-binary votour rocq.x86_64: W: no-documentation rocq-coqide-server.x86_64: W: no-documentation rocq-coqide-server-devel.x86_64: W: no-documentation rocq-core.x86_64: W: no-documentation rocq-core-source.x86_64: W: no-documentation rocq-runtime-devel.x86_64: W: no-documentation rocq.x86_64: E: no-binary rocq-doc.noarch: W: invalid-license OPUBL-1.0 rocq-runtime.x86_64: E: incorrect-fsf-address /usr/share/licenses/rocq-runtime/LICENSE rocq-doc.noarch: W: hidden-file-or-dir /usr/share/doc/rocq/refman-html/.doctrees rocq-doc.noarch: W: hidden-file-or-dir /usr/share/doc/rocq/refman-html/.doctrees rocq-rocqide.x86_64: W: files-duplicate /usr/share/icons/hicolor/256x256/mimetypes/rocqfile.png /usr/share/coq/coq.png:/usr/share/icons/hicolor/256x256/apps/rocq.png rocq.x86_64: E: explicit-lib-dependency ocaml-findlib rocq-rocqide.x86_64: W: desktopfile-without-binary /usr/share/applications/org.rocq-prover.rocqide.desktop coqide rocq.spec:284: W: configure-without-libdir-spec coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coq_makefile coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqc coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqchk coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqdep coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqdoc coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqnative coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqtop coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqtop.byte coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqworkmgr rocq-coqide-server.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqidetop rocq-rocqide.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/rocqide rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/csdpcert rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/ocamllibdep rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/rocq rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/rocqchk rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/votour rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/lib64/ocaml/rocq-runtime/rocqnative rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/lib64/ocaml/rocq-runtime/rocqworker 11 packages and 0 specfiles checked; 123 errors, 39 warnings, 4555 filtered, 123 badness; has taken 61.5 s Rpmlint (debuginfo) ------------------- Checking: rocq-coqide-server-debuginfo-9.1.1-1.fc45.x86_64.rpm rocq-runtime-debuginfo-9.1.1-1.fc45.x86_64.rpm rocq-debuginfo-9.1.1-1.fc45.x86_64.rpm rocq-rocqide-debuginfo-9.1.1-1.fc45.x86_64.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/tmp826m8_ee')] checks: 32, packages: 4 4 packages and 0 specfiles checked; 0 errors, 0 warnings, 163 filtered, 0 badness; has taken 10.8 s Rpmlint (installed packages) ---------------------------- ============================ 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: 14 rocq-rocqide.x86_64: E: zero-length /usr/lib64/ocaml/rocqide/META rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/btauto/g_btauto.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/cc/g_congruence.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/derive/g_derive.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/ltac/g_eqdecide.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/ltac/profile_ltac_tactics.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/nsatz/g_nsatz.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/rtauto/g_rtauto.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto.mli rocq-runtime-devel.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/plugins/zify/g_zify.mli rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Array/ArrayAxioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Array/PrimArray.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/BinNums/IntDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/BinNums/NatDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/BinNums/PosDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/CMorphisms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/CRelationClasses.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Equivalence.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Init.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Morphisms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/Morphisms_Prop.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/RelationClasses.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Classes/SetoidTactics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Coq818.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Coq819.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Coq820.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Compat/Rocq90.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/FloatAxioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/FloatClass.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/FloatOps.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/PrimFloat.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Floats/SpecFloat.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Byte.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Datatypes.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Decimal.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Hexadecimal.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Logic.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Ltac.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Nat.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Notations.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Number.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Peano.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Prelude.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Specif.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Sumbool.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Tactics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Tauto.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Init/Wf.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Lists/ListDef.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/BinNums.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/CarryType.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/PrimInt63.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Sint63Axioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Numbers/Cyclic/Int63/Uint63Axioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Basics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Tactics.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Utils.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Program/Wf.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Relations/Relation_Definitions.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Setoids/Setoid.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Strings/PrimString.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/Strings/PrimStringAxioms.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/derive/Derive.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/extraction/ExtrHaskellBasic.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/extraction/ExtrOcamlBasic.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/extraction/Extraction.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrbool.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrclasses.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssreflect.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrfun.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrsetoid.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssr/ssrunder.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/theories/ssrmatching/ssrmatching.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Array.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Bool.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Char.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq818.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Compat/Coq819.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Constant.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Constr.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Constructor.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Control.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Env.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Evar.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/FMap.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/FSet.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Float.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Fresh.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ident.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ind.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Init.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Int.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Lazy.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/List.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac1CompatNotations.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ltac2.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Message.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Meta.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Notations.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Option.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Pattern.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Printf.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Proj.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Pstring.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/RedFlags.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Ref.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Rewrite.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Std.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/String.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/TransparentState.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Uint63.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/coq/user-contrib/Ltac2/Unification.vos rocq-core.x86_64: E: zero-length /usr/lib64/ocaml/rocq-core/META rocq-runtime.x86_64: E: zero-length /usr/lib64/ocaml/rocq-runtime/revision rocq-coqide-server.x86_64: W: undefined-non-weak-symbol /usr/lib64/ocaml/coqide-server/core/core.cmxs camlCamlinternalOO.public_method_label_129_closure (/usr/lib64/ocaml/coqide-server/core/core.cmxs) ... [skipped million more of these undefined-non-weak-sumbol which is expected from Ocaml app] rocq-runtime.x86_64: W: undefined-non-weak-symbol /usr/lib64/ocaml/stublibs/dllcoqrun_stubs.so caml_failwith (/usr/lib64/ocaml/stublibs/dllcoqrun_stubs.so) rocq-runtime-devel.x86_64: E: static-library-without-debuginfo /usr/lib64/ocaml/rocq-runtime/vm/coqrun.a rocq.x86_64: E: spelling-error ('homotopy', '%description -l en_US homotopy -> photocopy') coq-core-compat.x86_64: E: spelling-error ('Rocq', '%description -l en_US Rocq -> Rock, Rococo') rocq-runtime.x86_64: E: spelling-error ('prover', '%description -l en_US prover -> prove, rover, proverb') rocq-doc.noarch: W: python-sphinx-doctrees-leftover /usr/share/doc/rocq/refman-html/.doctrees rocq-coqide-server.x86_64: W: no-manual-page-for-binary coqidetop coq-core-compat.x86_64: W: no-manual-page-for-binary coqpp coq-core-compat.x86_64: W: no-manual-page-for-binary coqtop.byte coq-core-compat.x86_64: W: no-manual-page-for-binary coqworkmgr rocq-runtime.x86_64: W: no-manual-page-for-binary csdpcert rocq-runtime.x86_64: W: no-manual-page-for-binary ocamllibdep rocq-runtime.x86_64: W: no-manual-page-for-binary rocq.byte rocq-runtime.x86_64: W: no-manual-page-for-binary votour rocq.x86_64: W: no-documentation rocq-coqide-server.x86_64: W: no-documentation rocq-core-source.x86_64: W: no-documentation rocq-runtime-devel.x86_64: W: no-documentation rocq-coqide-server-devel.x86_64: W: no-documentation rocq-core.x86_64: W: no-documentation rocq.x86_64: E: no-binary rocq-doc.noarch: W: invalid-license OPUBL-1.0 rocq-runtime.x86_64: E: incorrect-fsf-address /usr/share/licenses/rocq-runtime/LICENSE rocq-doc.noarch: W: hidden-file-or-dir /usr/share/doc/rocq/refman-html/.doctrees rocq-doc.noarch: W: hidden-file-or-dir /usr/share/doc/rocq/refman-html/.doctrees rocq-rocqide.x86_64: W: files-duplicate /usr/share/icons/hicolor/256x256/mimetypes/rocqfile.png /usr/share/coq/coq.png:/usr/share/icons/hicolor/256x256/apps/rocq.png rocq.x86_64: E: explicit-lib-dependency ocaml-findlib rocq-rocqide.x86_64: W: desktopfile-without-binary /usr/share/applications/org.rocq-prover.rocqide.desktop coqide rocq-rocqide.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/rocqide rocq-coqide-server.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqidetop coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coq_makefile coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqc coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqchk coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqdep coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqdoc coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqnative coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqtop coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqtop.byte coq-core-compat.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/coqworkmgr rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/csdpcert rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/ocamllibdep rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/rocq rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/rocqchk rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/bin/votour rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/lib64/ocaml/rocq-runtime/rocqnative rocq-runtime.x86_64: W: binary-or-shlib-calls-gethostbyname /usr/lib64/ocaml/rocq-runtime/rocqworker 14 packages and 0 specfiles checked; 122 errors, 22240 warnings, 4771 filtered, 122 badness; has taken 60.5 s Unversioned so-files -------------------- rocq-runtime: /usr/lib64/ocaml/stublibs/dllcoqperf_stubs.so rocq-runtime: /usr/lib64/ocaml/stublibs/dllcoqrun_stubs.so Source checksums ---------------- https://github.com/rocq-prover/rocq/archive/V9.1.1/rocq-9.1.1.tar.gz : CHECKSUM(SHA256) this package : 35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759 CHECKSUM(SHA256) upstream package : 35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759 Requires -------- rocq (rpmlib, GLIBC filtered): csdp-tools ocaml-findlib rocq-core(x86-64) rocq-runtime(x86-64) rocq-runtime (rpmlib, GLIBC filtered): /usr/bin/ocamlrun /usr/bin/python3 libc.so.6()(64bit) libgmp.so.10()(64bit) libm.so.6()(64bit) ocaml(Abbreviation) ... [skipped million Ocaml(...) deps] Generated by fedora-review 0.11.0 (05c5b26) last change: 2025-11-29 Command line :/usr/bin/fedora-review -v -b 2445873 --mock-config fedora-rawhide-x86_64 Buildroot used: fedora-rawhide-x86_64 Active plugins: C/C++, Shell-api, Generic Disabled plugins: Ocaml, SugarActivity, Perl, Python, Haskell, R, Java, PHP, fonts Disabled flags: EXARCH, EPEL6, EPEL7, DISTTAG, BATCH The package surely needs some love but it works well already so I consider it ================ === APPROVED === ================
Thank you very much for the review! I owe you. Let me know the next time you have a package up for review. I will go through the rpmlint messages. I see at least a few that should be addressed before I import this package.
The Pagure repository was created at https://src.fedoraproject.org/rpms/rocq
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.