On a freshly installed Fedora 43 system, this is what I get when installing the Coq proof assistant (without weak dependencies):
$ sudo dnf install --setopt=install_weak_deps=False coq
Updating and loading repositories:
Repositories loaded.
Package Arch Version Reposit Size
Installing:
coq x86_64 8.20.1-5.fc43 fedora 78.7 MiB
Installing dependencies:
add-determinism x86_64 0.6.0-2.fc43 fedora 2.4 MiB
annobin-docs noarch 12.99-1.fc43 fedora 98.9 KiB
annobin-plugin-gcc x86_64 12.99-1.fc43 fedora 1.0 MiB
ansible-srpm-macros noarch 1-18.1.fc43 fedora 35.7 KiB
build-reproducibility-srpm-macros noarch 0.6.0-2.fc43 fedora 735.0 B
coq-core x86_64 8.20.1-5.fc43 fedora 713.5 MiB
csdp x86_64 6.2.0-34.20181018git0dcf fedora 452.2 KiB
csdp-tools x86_64 6.2.0-34.20181018git0dcf fedora 62.5 KiB
dwz x86_64 0.16-2.fc43 fedora 287.1 KiB
efi-srpm-macros noarch 6-4.fc43 fedora 40.1 KiB
filesystem-srpm-macros noarch 3.18-50.fc43 fedora 38.2 KiB
flexiblas x86_64 3.5.0-1.fc43 updates 38.0 KiB
flexiblas-netlib x86_64 3.5.0-1.fc43 updates 16.5 MiB
flexiblas-openblas-openmp x86_64 3.5.0-1.fc43 updates 39.2 KiB
fonts-srpm-macros noarch 1:2.0.5-23.fc43 fedora 55.8 KiB
forge-srpm-macros noarch 0.4.0-3.fc43 fedora 38.9 KiB
fpc-srpm-macros noarch 1.3-15.fc43 fedora 144.0 B
gap-srpm-macros noarch 2-1.fc43 fedora 2.1 KiB
gcc-plugin-annobin x86_64 15.2.1-3.fc43 updates 57.2 KiB
ghc-srpm-macros noarch 1.9.2-3.fc43 fedora 779.0 B
gmp-c++ x86_64 1:6.3.0-4.fc43 fedora 27.6 KiB
gmp-devel x86_64 1:6.3.0-4.fc43 fedora 352.3 KiB
gnat-srpm-macros noarch 6-8.fc43 fedora 1.0 KiB
go-srpm-macros noarch 3.8.0-1.fc43 fedora 61.9 KiB
gpgverify noarch 2.2-3.fc43 fedora 8.7 KiB
java-srpm-macros noarch 1-7.fc43 fedora 870.0 B
kernel-srpm-macros noarch 1.0-27.fc43 fedora 1.9 KiB
libgfortran x86_64 15.2.1-3.fc43 updates 3.4 MiB
libquadmath x86_64 15.2.1-3.fc43 updates 317.9 KiB
libzstd-devel x86_64 1.5.7-2.fc43 fedora 208.0 KiB
lua-srpm-macros noarch 1-16.fc43 fedora 1.3 KiB
ocaml x86_64 5.3.0-4.fc43 fedora 167.7 MiB
ocaml-compiler-libs x86_64 5.3.0-4.fc43 fedora 110.3 MiB
ocaml-findlib x86_64 1.9.8-4.fc43 fedora 3.5 MiB
ocaml-runtime x86_64 5.3.0-4.fc43 fedora 4.4 MiB
ocaml-srpm-macros noarch 11-2.fc43 fedora 1.9 KiB
ocaml-zarith x86_64 1.14-8.fc43 fedora 375.9 KiB
ocaml-zarith-devel x86_64 1.14-8.fc43 fedora 1.1 MiB
openblas x86_64 0.3.29-2.fc43 fedora 111.7 KiB
openblas-openmp x86_64 0.3.29-2.fc43 fedora 43.7 MiB
openblas-srpm-macros noarch 2-20.fc43 fedora 112.0 B
package-notes-srpm-macros noarch 0.5-14.fc43 fedora 1.6 KiB
perl-srpm-macros noarch 1-60.fc43 fedora 861.0 B
pyproject-srpm-macros noarch 1.18.4-1.fc43 fedora 1.9 KiB
python-srpm-macros noarch 3.14-5.fc43 fedora 51.5 KiB
qt5-srpm-macros noarch 5.15.17-2.fc43 fedora 500.0 B
qt6-srpm-macros noarch 6.10.0-1.fc43 updates 464.0 B
redhat-rpm-config noarch 343-11.fc43 fedora 182.9 KiB
rust-srpm-macros noarch 26.4-1.fc43 fedora 4.8 KiB
texlive-base x86_64 11:20230311-93.fc43 fedora 19.0 MiB
tree-sitter-srpm-macros noarch 0.4.2-1.fc43 fedora 8.3 KiB
zig-srpm-macros noarch 1-5.fc43 fedora 1.1 KiB
Transaction Summary:
Installing: 53 packages
Total size of inbound packages is 366 MiB. Need to download 366 MiB.
After this operation, 1 GiB extra will be used (install 1 GiB, remove 0 B).
-
Why does it depend on tons of packages like
*-srpm-macrosandadd-determinism? These sound like they might be necessary at build time but I don’t see what could need them at runtime. Especially stuff related to Lua, Java, Perl, Qt, Rust, Zig, for which I don’t see a link with Coq (now renamed to Rocq but Fedora’s version is older than the renaming), which is a proof assistant implemented in OCaml. -
How can I trace back the dependency chain that led to their inclusion? Various Web pages suggested
dnf repoquery --treebut that option doesn’t appear to exist in the current version of DNF. I trieddnf repoquery --requires coqthen doing the same thing on the dependencies that this listed, but this gave a much smaller tree that didn’t include all the stuff above.