Bug 2445873

Summary: Review Request: rocq - Proof management system
Product: [Fedora] Fedora Reporter: Jerry James <loganjerry>
Component: Package ReviewAssignee: Peter Lemenkov <lemenkov>
Status: RELEASE_PENDING --- QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: medium Docs Contact:
Priority: medium    
Version: rawhideCC: lemenkov, package-review
Target Milestone: ---Flags: lemenkov: fedora-review+
Target Release: ---   
Hardware: All   
OS: Linux   
Whiteboard:
Fixed In Version: Doc Type: ---
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:
Bug Depends On:    
Bug Blocks: 2445874    

Description Jerry James 2026-03-09 21:34:00 UTC 
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.
Comment 1 Fedora Review Service 2026-03-09 21:54:31 UTC 
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.
Comment 2 Peter Lemenkov 2026-03-19 09:09:08 UTC 
I'll review it
Comment 3 Peter Lemenkov 2026-03-19 22:54:56 UTC 
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 ===
================
Comment 4 Jerry James 2026-03-20 01:24:27 UTC 
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.
Comment 5 Fedora Admin user for bugzilla script actions 2026-03-20 02:23:14 UTC 
The Pagure repository was created at https://src.fedoraproject.org/rpms/rocq