Contents

Make a skeleton spec file

We are going to create a package for verit. You don’t have to understand what verit does. The point is to show the steps needed to create an RPM package for a C project that uses autoconf and automake.

First, change to the directory where you want the RPM spec file to be created.

cd ~/rpmbuild/SPECS

One of the packages we had you install in setup is rpmdevtools, which contains several useful utilities for working with RPM packages. One of those tools is rpmdev-newspec, which creates a skeleton spec file for you. It has a number of templates which it uses to create the spec files; look in /etc/rpmdevtools to see the available templates. We will use the minimal template.

rpmdev-newspec verit

Now there is a file named verit.spec in your current directory. Let’s see what is inside.

Name:           verit
Version:
Release:        1%{?dist}
Summary:

License:
URL:
Source0:

BuildRequires:
Requires:

%description


%prep
%autosetup


%build
%configure
%make_build


%install
%make_install


%files
%license add-license-file-here
%doc add-docs-here



%changelog
* Thu Sep 25 2025 Jerry James
-

Determine the version

Let’s start filling in the spec file. First, what version are we packaging? At the time of this writing, the latest released version is 2024.12.1, so add that to the Version: line. While most software, including verit, now carries version numbers of the form number.number[.number], that style is not universal. If you are making a package for an upstream that has an unusual version numbering style, see the versioning guidelines for help on determining what to put in the Version: field.

Use autochangelog

Autochangelog is a recent addition to Fedora. It lets you avoid dealing directly with the Release: field and the %changelog section. Change the Release: field to read %autorelease. At the end of the spec file, replace the lines after %changelog with %autochangelog.

Write a summary

Next we need a summary. What does this package do? The home page says:

An open, trustable and efficient SMT-solver

Let’s reduce that to just “SMT solver” (Fedora already has a handful of these). Notice that there is no period in the summary. It is not a complete sentence, but rather a short descriptive phrase.

Determine the license

If you haven’t yet downloaded the tarball for the version you are packaging, do so now. Unpack the sources, and run licensecheck on the source files, as described here. In the case of verit 2024.12.1, the output looks like this:

./AUTHORS: *No copyright* UNKNOWN
./LICENSE: BSD 3-Clause License
./Makefile.am: *No copyright* UNKNOWN
./Makefile.in: UNKNOWN [generated file]
./README.md: *No copyright* UNKNOWN
./README_DEV.md: *No copyright* UNKNOWN
./aclocal.m4: FSF Unlimited License (with License Retention) [generated file]
./compile: GNU General Public License v2.0 or later [generated file]
./configure: FSF Unlimited License [generated file]
./configure.ac: *No copyright* UNKNOWN
./depcomp: GNU General Public License v2.0 or later [generated file]
./install-sh: X11 License [generated file]
./missing: GNU General Public License v2.0 or later [generated file]
./example/prepro.smt2: *No copyright* UNKNOWN
./example/xor_unsound.smt2: *No copyright* UNKNOWN
./m4/m4_ax_check_compile_flag.m4: FSF All Permissive License
./m4/m4_ax_prog_bison.m4: GNU General Public License v2.0 or later
./scripts/compile: GNU General Public License v2.0 or later [generated file]
./scripts/depcomp: GNU General Public License v2.0 or later [generated file]
./scripts/install-sh: X11 License [generated file]
./scripts/missing: GNU General Public License v2.0 or later [generated file]
./scripts/tap-driver.sh: GNU General Public License v2.0 or later [generated file]
./scripts/test-driver: GNU General Public License v2.0 or later [generated file]
./src/Makefile.am: *No copyright* UNKNOWN
./src/complete.c: *No copyright* UNKNOWN
./src/complete.h: *No copyright* UNKNOWN
./src/config.h.in: *No copyright* UNKNOWN
./src/hint.c: *No copyright* UNKNOWN
./src/hint.h: *No copyright* UNKNOWN
./src/main.c: *No copyright* UNKNOWN
./src/response.c: *No copyright* UNKNOWN
./src/response.h: *No copyright* UNKNOWN
./src/undo.c: *No copyright* UNKNOWN
./src/undo.h: *No copyright* UNKNOWN
./src/veriT-config.h: *No copyright* UNKNOWN
./src/veriT-state.c: *No copyright* UNKNOWN
./src/veriT-state.h: *No copyright* UNKNOWN
./src/veriT.c: *No copyright* UNKNOWN
./src/veriT.h: *No copyright* UNKNOWN
./test/Makefile.am: *No copyright* UNKNOWN
./test/main.c: *No copyright* UNKNOWN
./test/picotest.h: BSD 3-Clause License
./example/define-fun/cnst.smt2: *No copyright* UNKNOWN
./example/define-fun/eq.smt2: *No copyright* UNKNOWN
./example/proof/la_test.smt2: *No copyright* UNKNOWN
./example/proof/la_test_2.smt2: *No copyright* UNKNOWN
./example/proof/la_test_2p.smt2: *No copyright* UNKNOWN
./example/proof/la_test_3.smt2: *No copyright* UNKNOWN
./example/proof/la_test_4.smt2: *No copyright* UNKNOWN
./example/proof/la_test_p.smt2: *No copyright* UNKNOWN
./example/proof/qnt-simplify_1.smt2: *No copyright* UNKNOWN
./example/proof/quant-clausify_1.smt2: *No copyright* UNKNOWN
./example/proof/quant-clausify_2.smt2: *No copyright* UNKNOWN
./example/proof/step-simp_1.smt2: *No copyright* UNKNOWN
./example/proof/step-simp_2.smt2: *No copyright* UNKNOWN
./example/proof/step-simp_3.smt2: *No copyright* UNKNOWN
./example/proof/test_and_pos_rule.smt2: *No copyright* UNKNOWN
./example/proof/test_and_rule.smt2: *No copyright* UNKNOWN
./example/proof/test_not_or_rule.smt2: *No copyright* UNKNOWN
./example/proof/test_or_neg_rule.smt2: *No copyright* UNKNOWN
./src/SAT/veriT-SAT.c: *No copyright* UNKNOWN
./src/SAT/veriT-SAT.h: *No copyright* UNKNOWN
./src/arith/LA-hw.c: *No copyright* UNKNOWN
./src/arith/LA-hw.h: *No copyright* UNKNOWN
./src/arith/LA-mp.c: *No copyright* UNKNOWN
./src/arith/LA-mp.h: *No copyright* UNKNOWN
./src/arith/LA-pre.c: *No copyright* UNKNOWN
./src/arith/LA-pre.h: *No copyright* UNKNOWN
./src/arith/LA-xx.c.tpl: *No copyright* UNKNOWN
./src/arith/LA-xx.h.tpl: *No copyright* UNKNOWN
./src/arith/LA.c: *No copyright* UNKNOWN
./src/arith/LA.h: *No copyright* UNKNOWN
./src/arith/eq-store.c: *No copyright* UNKNOWN
./src/arith/eq-store.h: *No copyright* UNKNOWN
./src/arith/gcd-cache.def: *No copyright* UNKNOWN
./src/arith/numbers-hw.c: *No copyright* UNKNOWN
./src/arith/numbers-hw.h: *No copyright* UNKNOWN
./src/arith/numbers-mp.c: *No copyright* UNKNOWN
./src/arith/numbers-mp.h: *No copyright* UNKNOWN
./src/arith/numbers-xx.h.tpl: *No copyright* UNKNOWN
./src/arith/simplex-hw.c: *No copyright* UNKNOWN
./src/arith/simplex-hw.h: *No copyright* UNKNOWN
./src/arith/simplex-mp.c: *No copyright* UNKNOWN
./src/arith/simplex-mp.h: *No copyright* UNKNOWN
./src/arith/simplex-xx.c.tpl: *No copyright* UNKNOWN
./src/arith/simplex-xx.h.tpl: *No copyright* UNKNOWN
./src/arith/simplex.c: *No copyright* UNKNOWN
./src/arith/simplex.h: *No copyright* UNKNOWN
./src/arith/totality.c: *No copyright* UNKNOWN
./src/arith/totality.h: *No copyright* UNKNOWN
./src/bool/bool.c: *No copyright* UNKNOWN
./src/bool/bool.h: *No copyright* UNKNOWN
./src/bool/clause.c: *No copyright* UNKNOWN
./src/bool/cnf.c: *No copyright* UNKNOWN
./src/bool/cnf.c.tpl: *No copyright* UNKNOWN
./src/bool/cnf.h: *No copyright* UNKNOWN
./src/bool/literal.c: *No copyright* UNKNOWN
./src/bool/literal.h: *No copyright* UNKNOWN
./src/congruence/congruence.c: *No copyright* UNKNOWN
./src/congruence/congruence.h: *No copyright* UNKNOWN
./src/instantiation/ccfv-bckt.c: *No copyright* UNKNOWN
./src/instantiation/ccfv-bckt.h: *No copyright* UNKNOWN
./src/instantiation/ccfv-constr.c: *No copyright* UNKNOWN
./src/instantiation/ccfv-constr.h: *No copyright* UNKNOWN
./src/instantiation/ccfv-mod.c: *No copyright* UNKNOWN
./src/instantiation/ccfv-mod.h: *No copyright* UNKNOWN
./src/instantiation/ccfv.c: *No copyright* UNKNOWN
./src/instantiation/ccfv.h: *No copyright* UNKNOWN
./src/instantiation/discrimination-tree.c: *No copyright* UNKNOWN
./src/instantiation/discrimination-tree.h: *No copyright* UNKNOWN
./src/instantiation/free-vars.c: *No copyright* UNKNOWN
./src/instantiation/free-vars.h: *No copyright* UNKNOWN
./src/instantiation/inst-create.c: *No copyright* UNKNOWN
./src/instantiation/inst-create.h: *No copyright* UNKNOWN
./src/instantiation/inst-del.c: *No copyright* UNKNOWN
./src/instantiation/inst-del.h: *No copyright* UNKNOWN
./src/instantiation/inst-enum.c: *No copyright* UNKNOWN
./src/instantiation/inst-enum.h: *No copyright* UNKNOWN
./src/instantiation/inst-index.c: *No copyright* UNKNOWN
./src/instantiation/inst-index.h: *No copyright* UNKNOWN
./src/instantiation/inst-man.c: *No copyright* UNKNOWN
./src/instantiation/inst-man.h: *No copyright* UNKNOWN
./src/instantiation/inst-pre.c: *No copyright* UNKNOWN
./src/instantiation/inst-pre.h: *No copyright* UNKNOWN
./src/instantiation/inst-strategy.h: *No copyright* UNKNOWN
./src/instantiation/inst-symbs.c: *No copyright* UNKNOWN
./src/instantiation/inst-symbs.h: *No copyright* UNKNOWN
./src/instantiation/inst-trigger-selection.c: *No copyright* UNKNOWN
./src/instantiation/inst-trigger-selection.h: *No copyright* UNKNOWN
./src/instantiation/inst-trigger.c: *No copyright* UNKNOWN
./src/instantiation/inst-trigger.h: *No copyright* UNKNOWN
./src/instantiation/syntactic-unify.c: *No copyright* UNKNOWN
./src/instantiation/syntactic-unify.h: *No copyright* UNKNOWN
./src/instantiation/ujobs.c: *No copyright* UNKNOWN
./src/instantiation/ujobs.h: *No copyright* UNKNOWN
./src/instantiation/unify.c: *No copyright* UNKNOWN
./src/instantiation/unify.h: *No copyright* UNKNOWN
./src/pre/HOL.c: *No copyright* UNKNOWN
./src/pre/HOL.h: *No copyright* UNKNOWN
./src/pre/bclauses.c: *No copyright* UNKNOWN
./src/pre/bclauses.h: *No copyright* UNKNOWN
./src/pre/bfun-elim.c: *No copyright* UNKNOWN
./src/pre/bfun-elim.h: *No copyright* UNKNOWN
./src/pre/binder-rename.c: *No copyright* UNKNOWN
./src/pre/binder-rename.h: *No copyright* UNKNOWN
./src/pre/connectives.c: *No copyright* UNKNOWN
./src/pre/connectives.h: *No copyright* UNKNOWN
./src/pre/distinct-elim.c: *No copyright* UNKNOWN
./src/pre/distinct-elim.h: *No copyright* UNKNOWN
./src/pre/fix-trigger.c: *No copyright* UNKNOWN
./src/pre/fix-trigger.h: *No copyright* UNKNOWN
./src/pre/ite-elim.c: *No copyright* UNKNOWN
./src/pre/ite-elim.h: *No copyright* UNKNOWN
./src/pre/let-elim.c: *No copyright* UNKNOWN
./src/pre/let-elim.h: *No copyright* UNKNOWN
./src/pre/nary-elim.c: *No copyright* UNKNOWN
./src/pre/nary-elim.h: *No copyright* UNKNOWN
./src/pre/pm.c: *No copyright* UNKNOWN
./src/pre/pm.h: *No copyright* UNKNOWN
./src/pre/pre.c: *No copyright* UNKNOWN
./src/pre/pre.h: *No copyright* UNKNOWN
./src/pre/qnt-tidy.c: *No copyright* UNKNOWN
./src/pre/qnt-tidy.h: *No copyright* UNKNOWN
./src/pre/qnt-trigger.c: *No copyright* UNKNOWN
./src/pre/qnt-trigger.h: *No copyright* UNKNOWN
./src/pre/qsimp-by-unification.c: *No copyright* UNKNOWN
./src/pre/qsimp-by-unification.h: *No copyright* UNKNOWN
./src/pre/rare-symb.c: *No copyright* UNKNOWN
./src/pre/rare-symb.h: *No copyright* UNKNOWN
./src/pre/simp-formula-sat.c: *No copyright* UNKNOWN
./src/pre/simp-formula-sat.h: *No copyright* UNKNOWN
./src/pre/simp-node-proof.c: *No copyright* UNKNOWN
./src/pre/simp-node-proof.h: *No copyright* UNKNOWN
./src/pre/simp-sym.c: *No copyright* UNKNOWN
./src/pre/simp-sym.h: *No copyright* UNKNOWN
./src/pre/simp-unit.c: *No copyright* UNKNOWN
./src/pre/simp-unit.h: *No copyright* UNKNOWN
./src/pre/simplify-AC.c: *No copyright* UNKNOWN
./src/pre/simplify-AC.h: *No copyright* UNKNOWN
./src/pre/simplify.c: *No copyright* UNKNOWN
./src/pre/simplify.h: *No copyright* UNKNOWN
./src/pre/skolem.c: *No copyright* UNKNOWN
./src/pre/skolem.h: *No copyright* UNKNOWN
./src/proof/proof-checking.c: *No copyright* UNKNOWN
./src/proof/proof-checking.h: *No copyright* UNKNOWN
./src/proof/proof-id.c: *No copyright* UNKNOWN
./src/proof/proof-id.h: *No copyright* UNKNOWN
./src/proof/proof-lemma-hash.c: *No copyright* UNKNOWN
./src/proof/proof-lemma-hash.h: *No copyright* UNKNOWN
./src/proof/proof-output.c: *No copyright* UNKNOWN
./src/proof/proof-output.h: *No copyright* UNKNOWN
./src/proof/proof-print.c: *No copyright* UNKNOWN
./src/proof/proof-print.h: *No copyright* UNKNOWN
./src/proof/proof-rules-tautologies.c: *No copyright* UNKNOWN
./src/proof/proof-rules-tautologies.h: *No copyright* UNKNOWN
./src/proof/proof-rules.c: *No copyright* UNKNOWN
./src/proof/proof-rules.h: *No copyright* UNKNOWN
./src/proof/proof-sat-solver.c: *No copyright* UNKNOWN
./src/proof/proof-sat-solver.h: *No copyright* UNKNOWN
./src/proof/proof-step-hash.c: *No copyright* UNKNOWN
./src/proof/proof-step-hash.h: *No copyright* UNKNOWN
./src/proof/proof-step-table.c: *No copyright* UNKNOWN
./src/proof/proof-step-table.h: *No copyright* UNKNOWN
./src/proof/proof-step.c: *No copyright* UNKNOWN
./src/proof/proof-step.h: *No copyright* UNKNOWN
./src/proof/proof-subproof.c: *No copyright* UNKNOWN
./src/proof/proof-subproof.h: *No copyright* UNKNOWN
./src/proof/proof-type.c: *No copyright* UNKNOWN
./src/proof/proof-type.h: *No copyright* UNKNOWN
./src/proof/proof-unsat-core.c: *No copyright* UNKNOWN
./src/proof/proof-unsat-core.h: *No copyright* UNKNOWN
./src/proof/proof.c: *No copyright* UNKNOWN
./src/proof/proof.h: *No copyright* UNKNOWN
./src/symbolic/DAG-arith.c: *No copyright* UNKNOWN
./src/symbolic/DAG-arith.h: *No copyright* UNKNOWN
./src/symbolic/DAG-flag.c: *No copyright* UNKNOWN
./src/symbolic/DAG-flag.h: *No copyright* UNKNOWN
./src/symbolic/DAG-print.c: *No copyright* UNKNOWN
./src/symbolic/DAG-print.h: *No copyright* UNKNOWN
./src/symbolic/DAG-prop.c: *No copyright* UNKNOWN
./src/symbolic/DAG-prop.h: *No copyright* UNKNOWN
./src/symbolic/DAG-ptr.h: *No copyright* UNKNOWN
./src/symbolic/DAG-smtlib.c: *No copyright* UNKNOWN
./src/symbolic/DAG-sort-pm.c: *No copyright* UNKNOWN
./src/symbolic/DAG-sort-pm.h: *No copyright* UNKNOWN
./src/symbolic/DAG-sort.c: *No copyright* UNKNOWN
./src/symbolic/DAG-sort.h: *No copyright* UNKNOWN
./src/symbolic/DAG-stat.c: *No copyright* UNKNOWN
./src/symbolic/DAG-stat.h: *No copyright* UNKNOWN
./src/symbolic/DAG-subst.c: *No copyright* UNKNOWN
./src/symbolic/DAG-subst.h: *No copyright* UNKNOWN
./src/symbolic/DAG-symb-DAG.c: *No copyright* UNKNOWN
./src/symbolic/DAG-symb-DAG.h: *No copyright* UNKNOWN
./src/symbolic/DAG-symb.c: *No copyright* UNKNOWN
./src/symbolic/DAG-symb.h: *No copyright* UNKNOWN
./src/symbolic/DAG-tmp.c: *No copyright* UNKNOWN
./src/symbolic/DAG-tmp.h: *No copyright* UNKNOWN
./src/symbolic/DAG.c: *No copyright* UNKNOWN
./src/symbolic/DAG.h: *No copyright* UNKNOWN
./src/symbolic/context-handling.c: *No copyright* UNKNOWN
./src/symbolic/context-handling.h: *No copyright* UNKNOWN
./src/symbolic/context-recursion-proof.c: *No copyright* UNKNOWN
./src/symbolic/context-recursion-proof.h: *No copyright* UNKNOWN
./src/symbolic/context-recursion.c: *No copyright* UNKNOWN
./src/symbolic/context-recursion.h: *No copyright* UNKNOWN
./src/symbolic/dbg-trigger.c: *No copyright* UNKNOWN
./src/symbolic/dbg-trigger.h: *No copyright* UNKNOWN
./src/symbolic/polarities.c: *No copyright* UNKNOWN
./src/symbolic/polarities.h: *No copyright* UNKNOWN
./src/symbolic/qnt-utils.c: *No copyright* UNKNOWN
./src/symbolic/qnt-utils.h: *No copyright* UNKNOWN
./src/symbolic/recursion.c: *No copyright* UNKNOWN
./src/symbolic/recursion.h: *No copyright* UNKNOWN
./src/symbolic/veriT-DAG.h: *No copyright* UNKNOWN
./src/symbolic/veriT-status.h: *No copyright* UNKNOWN
./src/utils/assoc.h: *No copyright* UNKNOWN
./src/utils/bitset.c: *No copyright* UNKNOWN
./src/utils/bitset.h: *No copyright* UNKNOWN
./src/utils/dll-DAG.h: *No copyright* UNKNOWN
./src/utils/dll-TYPE.tpl: *No copyright* UNKNOWN
./src/utils/dll.c: *No copyright* UNKNOWN
./src/utils/dll.h: *No copyright* UNKNOWN
./src/utils/general.c: *No copyright* UNKNOWN
./src/utils/general.h: *No copyright* UNKNOWN
./src/utils/h-util.c: *No copyright* UNKNOWN
./src/utils/h-util.h: *No copyright* UNKNOWN
./src/utils/h.h: *No copyright* UNKNOWN
./src/utils/ha.c.tpl: *No copyright* UNKNOWN
./src/utils/hash.c: *No copyright* UNKNOWN
./src/utils/hash.h: *No copyright* UNKNOWN
./src/utils/hashmap.c: *No copyright* UNKNOWN
./src/utils/hashmap.h: *No copyright* UNKNOWN
./src/utils/hk.h: *No copyright* UNKNOWN
./src/utils/list.c: *No copyright* UNKNOWN
./src/utils/list.h: *No copyright* UNKNOWN
./src/utils/nonce.c: *No copyright* UNKNOWN
./src/utils/nonce.h: *No copyright* UNKNOWN
./src/utils/options.c: *No copyright* UNKNOWN
./src/utils/options.h: *No copyright* UNKNOWN
./src/utils/stack.h: *No copyright* UNKNOWN
./src/utils/statistics.c: *No copyright* UNKNOWN
./src/utils/statistics.h: *No copyright* UNKNOWN
./src/utils/sys.c: *No copyright* UNKNOWN
./src/utils/sys.h: *No copyright* UNKNOWN
./src/utils/table.c: *No copyright* UNKNOWN
./src/utils/table.h: *No copyright* UNKNOWN
./src/utils/types.h: *No copyright* UNKNOWN
./src/utils/veriT-qsort.c: BSD 3-Clause License
./src/utils/veriT-qsort.h: *No copyright* UNKNOWN
./src/utils/veriT-signal.c: *No copyright* UNKNOWN
./src/utils/veriT-signal.h: *No copyright* UNKNOWN
./src/veriT-SAT/main.c: *No copyright* UNKNOWN
./test/suits/discrimination-tree.h: *No copyright* UNKNOWN
./test/suits/syntactic-unify.h: *No copyright* UNKNOWN
./src/parsers/dimacs/dimacs.c: *No copyright* UNKNOWN
./src/parsers/dimacs/dimacs.h: *No copyright* UNKNOWN
./src/parsers/smtlib2/parser_macro.h: *No copyright* UNKNOWN
./src/parsers/smtlib2/smtfun.c: *No copyright* UNKNOWN
./src/parsers/smtlib2/smtfun.h: *No copyright* UNKNOWN
./src/parsers/smtlib2/smtlex.c: *No copyright* UNKNOWN
./src/parsers/smtlib2/smtlex.l: *No copyright* UNKNOWN
./src/parsers/smtlib2/smtlib2.h: *No copyright* UNKNOWN
./src/parsers/smtlib2/smtsyn.c: GNU General Public License v3.0 or later
./src/parsers/smtlib2/smtsyn.h: GNU General Public License v3.0 or later
./src/parsers/smtlib2/smtsyn.y: *No copyright* UNKNOWN
./src/parsers/smtlib2/smttypes.h: *No copyright* UNKNOWN

The toplevel LICENSE file contains a BSD license. The various autotools scripts can be ignored, as no part of them will appear in the final binary package. But what’s up with smtsyn.c and smtsyn.h? They seem to be GPL-3.0-or-later files. If we look into them, we find that these are files generated by bison. The license text at the top of those files tells us that an exception to that license applies.

The Fedora project uses SPDX License names. BSD-3-Clause is on the list, matching what licensecheck found in LICENSE and src/utils/veriT-qsort.c. The smtsyn.c license is GPL-3.0-or-later, but we also need to look at the License exceptions for that bison exception. It is on the list as Bison-exception-2.2. Therefore, the License: field should contain BSD-3-Clause AND GPL-3.0-or-later WITH Bison-exception-2.2.

The URL field

Next, put the project URL into the URL: field of the spec file. This should be some sort of home page for the project. In the verit case, the value of the field is https://www.verit-solver.org/. If the project is on github, the project URL may be the main repository page for the project, which will be a URL of the form https://github.com/owner/project. In that case, check whether either of the pages https://owner.github.io/project or https://owner.github.io/ exist and contain useful content. Use one of them as the URL if so.

The Source field

The Source fields in the spec file identify those files that must be present in the build root in order to build the software. See the Source URL guidelines for help determining the appropriate URL for this field.

The name of the package should be replaced with %{name} in this URL, and the version number should be replaced with %{version}. The intent is to avoid changing the URL field every time a new version is released.

For the verit package, we will use this as the Source URL:

%{url}/download/%{version}/%{name}-%{version}.tar.gz

where the %{url} macro expands to the contents of the URL field.

BuildRequires

Each BuildRequires tag in a spec file identifies some package that must be installed prior to building the target package. Let’s examine the verit package.

At the top level of the source directory, we see a file named configure.ac. This is an autoconf input file, and will often contain references to other packages needed to build this one. Under # Check programs, we see that the configure script checks for lex, awk, bison, and sed. Both awk (gawk) and sed are installed in the buildroot by default, but lex (flex) and bison are not, so add BuildRequires for both.

Under # Checks for libraries we see that the configure script wants to find the gmp library. There is a gmp-devel package, but be aware of the need to use pkgconfig requires in some cases. This does not appear to be one of those cases, so add BuildRequires: gmp-devel to the spec file.

Looking into the src subdirectory, we see that this project contains files with a .c suffix; i.e., they are C source files. We need a C compiler to build, then, so add BuildRequires: gcc to the spec file. Finally, as is common with autotools projects, a Makefile will be generated, so add BuildRequires: make to the spec file. It should now look like this:

Name:           verit
Version:        2024.12.1
Release:        %autorelease
Summary:        SMT solver

# BSD-3-Clause: the project as a whole
# GPL-3.0-or-later WITH Bison-exception-2.2: smtsyn.{c,h}
License:        BSD-3-Clause AND GPL-3.0-or-later WITH Bison-exception-2.2
URL:            https://www.verit-solver.org/
Source:         %{url}/download/%{version}/%{name}-%{version}.tar.gz

BuildRequires:  bison
BuildRequires:  flex
BuildRequires:  gcc
BuildRequires:  gmp-devel
BuildRequires:  make

%description

%prep
%autosetup


%build
%configure
%make_build


%install
%make_install


%files
%license add-license-file-here
%doc add-docs-here



%changelog
%autochangelog

Description

The %description section is typically filled in with text from a README file. Failing that, do your best to write a paragraph describing what this package does. You want a person who has never heard of the software before to be able to get some idea of the purpose of the package from reading the description. As noted in the packaging guidelines, keep lines to 80 characters or less. Longer lines can be displayed in strange ways in the various graphical software managers. I usually limit description lines to 78 characters to be on the safe side.

Prep

The %prep section is where we do anything that must be done prior to building the software. Typically, the first step is to unpack a tarball or zip file. The %autosetup macro is often sufficient. It knows how to unpack a variety of files and compression types. This macro assumes that, after unpacking, it will find the source files in a directory named %{name}-%{version}. If that is not the case, we need to tell it so. In the verit case, the name of the directory is verit2-2024.12.1, which matches what %autosetup expects.

Build

The %build section contains instructions on how to build the softare. The %configure and %make_build macros placed there by rpmdev-newspec are intended for use with software that supplies an autoconf-generated configure script. That’s perfect for us, so leave it as is.

Install

The %install section installs the software into a directory identified by the macro %buildroot. RPM uses the files placed there to build the final binary package. We have %make_install in the %install section. That macro runs make install with some flags that are commonly used to get the installed files to go into %buildroot. Like %configure and %make_build, it is intended for projects that use autoconf, so leave it alone and we’ll see if it does the job.

Files

The %files section lists all of the files that go into the binary RPM. We don’t have to guess; we’ll do a test build and install to help us figure this out. However, there are two things we can do right now. Since we see a file named LICENSE in the source directory, change the %license line to refer to it. Also, there are README.md and AUTHORS files, so change the %doc line to refer to them. The spec file should now look something like this:

Name:           verit
Version:        2024.12.1
Release:        %autorelease
Summary:        SMT solver

# BSD-3-Clause: the project as a whole
# GPL-3.0-or-later WITH Bison-exception-2.2: smtsyn.{c,h}
License:        BSD-3-Clause AND GPL-3.0-or-later WITH Bison-exception-2.2
URL:            https://www.verit-solver.org/
Source:         %{url}/download/%{version}/%{name}-%{version}.tar.gz

BuildRequires:  bison
BuildRequires:  flex
BuildRequires:  gcc
BuildRequires:  gmp-devel
BuildRequires:  make

%description
veriT is an SMT (Satisfiability Modulo Theories) solver.  It is open-source, 
proof-producing, and complete for quantifier-free formulas with uninterpreted 
functions and linear arithmetic on real numbers and integers.  It also offers 
good support for quantifiers.

This release is a remix of veriT adapted for usage inside proof assistants.  
Some features, especially non-linear arithmetic support, were removed.

The front-end uses the SMTLIB-2 language (documented at https://smt-lib.org/), 
but not all features are supported.

%prep
%autosetup

%build
%configure
%make_build

%install
%make_install

%files
%license LICENSE
%doc AUTHORS README.md

%changelog
%autochangelog

First test build

Make sure that your spec file is in ~/rpmbuild/SPECS, and that verit-2024.12.1.tar.gz is in ~/rpmbuild/SOURCES. While in the ~/rpmbuild/SPECS directory, run rpmbuild -bs verit.spec. That command generates a source rpm in ~/rpmbuild/SRPMS.

Next, we will attempt to build the package with mock. Refer to building with mock for details. Briefly, run this command:

mock -r fedora-rawhide-x86_64 --rebuild ~/rpmbuild/SRPMS/verit-2024.12.1-1.fc42.src.rpm

You may have to replace fc42 in that filename. Make it match the name of the file in your ~/rpmbuild/SRPMS directory.

The test build runs all the way to the end, giving us the list of installed files that we need for the %files section:

Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILD/verit-2024.12.1-build/BUILDROOT
error: Installed (but unpackaged) file(s) found:
   /usr/bin/veriT
   /usr/bin/veriT-SAT
   /usr/lib/debug/usr/bin/veriT-2024.12.1-1.fc44.x86_64.debug
   /usr/lib/debug/usr/bin/veriT-SAT-2024.12.1-1.fc44.x86_64.debug
    Installed (but unpackaged) file(s) found:
   /usr/bin/veriT
   /usr/bin/veriT-SAT
   /usr/lib/debug/usr/bin/veriT-2024.12.1-1.fc44.x86_64.debug
   /usr/lib/debug/usr/bin/veriT-SAT-2024.12.1-1.fc44.x86_64.debug

We can ignore the debug files as they will be handled automatically once we get everything else right. Add this to %files:

%{_bindir}/veriT
%{_bindir}/veriT-SAT

We’re done!

Build flags

Just kidding! Let’s look at that build log again. In particular, look at the build flags used for C source files. After the Fedora flags, you’ll see some flags inserted by veriT upstream:

-O3 -fomit-frame-pointer -finline-limit=1000000 -flto=auto

We don’t necessarily want all of upstream’s flags. In particular, Fedora chooses its own optimization flag (currently -O2), so we do not want the -O3. The choice of omitting the frame pointer or not is also made by Fedora, so we should also remove -fomit-frame-ponter. The inline-limit flag should be fine. Fedora also uses -flto=auto, so adding it a second time does no harm.

The configure script does not give us an option for eliminating -O3 or -fomit-frame-pointer however, so add this to %prep:

# Do not override Fedora flags.
sed -i '/-O3/d;/-fomit-frame-pointer/d' configure

Build again. The build is successful. At this point, the spec file should look something like this:

Name:           verit
Version:        2024.12.1
Release:        %autorelease
Summary:        SMT solver

# BSD-3-Clause: the project as a whole
# GPL-3.0-or-later WITH Bison-exception-2.2: smtsyn.{c,h}
License:        BSD-3-Clause AND GPL-3.0-or-later WITH Bison-exception-2.2
URL:            https://www.verit-solver.org/
Source:         %{url}/download/%{version}/%{name}-%{version}.tar.gz

BuildRequires:  gcc
BuildRequires:  gmp-devel
BuildRequires:  make

%description
veriT is an SMT (Satisfiability Modulo Theories) solver.  It is open-source, 
proof-producing, and complete for quantifier-free formulas with uninterpreted 
functions and linear arithmetic on real numbers and integers.  It also offers 
good support for quantifiers.

This release is a remix of veriT adapted for usage inside proof assistants.  
Some features, especially non-linear arithmetic support, were removed.

The front-end uses the SMTLIB-2 language (documented at https://smt-lib.org/), 
but not all features are supported.

%prep
%autosetup

# Do not override Fedora flags
sed -i '/-O3/d;/-fomit-frame-pointer/d' configure

%build
%configure
%make_build

%install
%make_install

%files
%license LICENSE
%doc AUTHORS README.md
%{_bindir}/veriT
%{_bindir}/veriT-SAT

%changelog
%autochangelog

Requires and Provides

Now that we have a reasonable looking package, lets make sure that the final Requires and Provides look right.

$ rpm -q --requires -p /var/lib/mock/fedora-rawhide-x86_64/result/verit-2024.12.1-1.fc44.x86_64.rpm
libc.so.6()(64bit)
libc.so.6(GLIBC_2.14)(64bit)
libc.so.6(GLIBC_2.2.5)(64bit)
libc.so.6(GLIBC_2.3)(64bit)
libc.so.6(GLIBC_2.3.4)(64bit)
libc.so.6(GLIBC_2.34)(64bit)
libc.so.6(GLIBC_2.38)(64bit)
libc.so.6(GLIBC_2.4)(64bit)
libc.so.6(GLIBC_ABI_DT_RELR)(64bit)
libgmp.so.10()(64bit)
libm.so.6()(64bit)
libm.so.6(GLIBC_2.29)(64bit)
rpmlib(CompressedFileNames) <= 3.0.4-1
rpmlib(FileDigests) <= 4.6.0-1
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
rpmlib(PayloadIsZstd) <= 5.4.18-1
rtld(GNU_HASH)

We see a dependency on gmp, which is good.

$ rpm -q --provides -p /var/lib/mock/fedora-rawhide-x86_64/result/verit-2024.12.1-1.fc44.x86_64.rpm
verit = 2024.12.1-1.fc44
verit(x86-64) = 2024.12.1-1.fc44

That looks good, too. Let’s take a peek at the contents of the binary RPM while we are at it.

$ rpm -qlp /var/lib/mock/fedora-rawhide-x86_64/result/verit-2024.12.1-1.fc44.x86_64.rpm
/usr/bin/veriT
/usr/bin/veriT-SAT
/usr/lib/.build-id
/usr/lib/.build-id/99
/usr/lib/.build-id/99/93cd40005d1075493a52c47480cfcf6bf49308
/usr/lib/.build-id/de
/usr/lib/.build-id/de/155531cc3ac547b6c7e90de5f1b89e28984526
/usr/share/doc/verit
/usr/share/doc/verit/AUTHORS
/usr/share/doc/verit/README.md
/usr/share/licenses/verit
/usr/share/licenses/verit/LICENSE

That looks fine.

Run tests

Upstream has provided us with some tests. We should run them to make sure we haven’t somehow broken the whole thing. With autotools projects, make check often does what we want. Let’s try it. Add this to the spec file:

%check
%make_build check

Run that again and the tests all pass. Great!

Run rpmlint

We finally have a viable spec file! Let’s run an automated tool over it that can detect many common packaging problems.

mock -r fedora-rawhide-x86_64 --install /var/lib/mock/fedora-rawhide-x86_64/result/*.x86_64.rpm rpmlint pam

Afterwards, we enter a mock shell:

mock -r fedora-rawhide-x86_64 --shell --enable-network

The --enable-network argument allows rpmlint to access the network in order to do some checks, such as URL validity. In the shell, run this command:

# rpmlint -i verit
================================================ rpmlint session starts ===============================================
rpmlint: 2.7.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: 1

verit.x86_64: W: no-manual-page-for-binary veriT
verit.x86_64: W: no-manual-page-for-binary veriT-SAT
=========== 1 packages and 0 specfiles checked; 0 errors, 2 warnings, 3 filtered, 0 badness; has taken 0.1 s ==========

There are indeed no man pages for these tools. Do the tools themselves provide any help? Try running veriT --help. Sure enough, we get a list of command line options. In that case, maybe we can construct useful man pages.

Generate a man page

The help2man package contains a useful tool that converts --help output to a man page. Exit from the mock shell, then run this command:

mock -r fedora-rawhide-x86_64 --install help2man

Then get a mock shell again:

mock -r fedora-rawhide-x86_64 --shell

Let’s see if we can find an invocation of help2man that generates a reasonable man page.

# su - mockbuild
$ cd build/BUILD/verit-2024.12.1-build/verit-2024.12.1
$ help2man ./veriT
help2man: can't get `--help' info from ./veriT
Try `--no-discard-stderr' if option outputs to stderr

We saw help output, so maybe help2man is right about it sending output to stderr. Let’s see:

$ help2man --no-discard-stderr ./veriT

That certainly looks like man page output. Let’s save it to a file so we can more easily work with it:

$ help2man --no-discard-stderr -o veriT.1 ./veriT
$ nroff -man veriT.1

That doesn’t look completely terrible. Let’s start going over it. Right away, we notice a problem on the first line of output:

THIS(1)                          User Commands                         THIS(1)

The command name is not “This”. The word “This” does not show up at the top of the veriT --help output. What is going on? Well, help2man also runs veriT --version to get the version number. Let’s see what that produces:

$ ./veriT --version
This is veriT, version 2024.12.1

Ah, that’s where “This” is coming from! Since help2man doesn’t know how to parse that, let’s pass the version number in directly.

$ help2man --no-discard-stderr -o veriT.1 --version-string=2024.12.1 ./veriT

That looks a lot better. But the NAME section could use some work:

NAME
       veriT - manual page for veriT 2024.12.1

That’s not very useful. Let’s try passing in some useful text for the name section.

help2man --no-discard-stderr -o veriT.1 --version-string=2021.06-rmx -n 'SMT solver' ./veriT

That looks much better. But what’s this section at the end?

SEE ALSO
       The full documentation for veriT is maintained as a Texinfo manual.  If
       the  info  and  veriT programs are properly installed at your site, the
       command

              info veriT

       should give you access to the complete manual.

That is boilerplate text for GNU projects, which do indeed maintain Texinfo manuals. Non-GNU projects typically do not, and this one is no exception. Fortunately, help2man has the -N flag to turn that off. The final invocation looks like this:

help2man --no-discard-stderr -o veriT.1 --version-string=2021.06-rmx -n 'SMT solver' -N ./veriT

The ‘Version’ line under DESCRIPTION is not useful, since man already displays the version number in another way. However, we cannot tell help2man to not include it, because it is simply part of the output of veriT --help. We may want to remove that line with a sed command. After reordering the help2man options in a way that makes sense to me, substituting %{version} for the bare version number in that command line, and splitting the long line, I inserted this into the spec file, at the end of the %build section:

# Build man page
help2man -N --no-discard-stderr --version-string=%{version}-rmx \
  -n 'SMT solver' -o veriT.1 ./veriT
sed -i '/Version: veriT/d' veriT.1

We need to install the man page in the %install section. Add this:

# Install man page
install -D -m 0644 veriT.1 %{buildroot}%{_mandir}/man1/veriT.1

We also need to add %{_mandir}/man1/veriT.1* to %files. Why the asterisk at the end? Because RPM compresses man pages, so a suffix will be added to the file. Currently, gzip is used, so the suffix is “.gz”, but I don’t want to gamble that that will be the case forever. Some day we may have xz-compressed man pages. With the asterisk I don’t have to worry about it.

Now let’s build a man for the other binary, veriT-SAT. Let’s see what its help output looks like.

$ ./veriT-SAT --help
s SATISFIABLE
v

Wait, what? Maybe I don’t understand what this binary does. Let’s look in the source directory, in src/veriT-SAT/main.c. Sure enough, there is no help text anywhere. Looking at the code in main() shows that it expects exactly one argument, a filename. The code parses the file as a SAT problem, solves it, and prints the result. We now have the choice of manually constructing a man page that says that, or omitting a man page for this binary. In the latter case, the final spec file looks like this:

Name:           verit
Version:        2024.12.1
Release:        %autorelease
Summary:        SMT solver

# BSD-3-Clause: the project as a whole
# GPL-3.0-or-later WITH Bison-exception-2.2: smtsyn.{c,h}
License:        BSD-3-Clause AND GPL-3.0-or-later WITH Bison-exception-2.2
URL:            https://www.verit-solver.org/
Source:         %{url}/download/%{version}/%{name}-%{version}.tar.gz

BuildRequires:  bison
BuildRequires:  flex
BuildRequires:  gcc
BuildRequires:  gmp-devel
BuildRequires:  help2man
BuildRequires:  make

%description
veriT is an SMT (Satisfiability Modulo Theories) solver.  It is open-source, 
proof-producing, and complete for quantifier-free formulas with uninterpreted 
functions and linear arithmetic on real numbers and integers.  It also offers 
good support for quantifiers.

This release is a remix of veriT adapted for usage inside proof assistants.  
Some features, especially non-linear arithmetic support, were removed.

The front-end uses the SMTLIB-2 language (documented at https://smt-lib.org/), 
but not all features are supported.

%prep
%autosetup

# Do not override Fedora flags
sed -i '/-O3/d;/-fomit-frame-pointer/d' configure

%build
%configure
%make_build

# Build man page
help2man -N --no-discard-stderr --version-string=%{version}-rmx \
  -n 'SMT solver' -o veriT.1 ./veriT
sed -i '/Version: veriT/d' veriT.1

%install
%make_install

# Install man page
install -D -m 0644 veriT.1 %{buildroot}%{_mandir}/man1/veriT.1

%check
%make_build check

%files
%license LICENSE
%doc AUTHORS README.md
%{_bindir}/veriT
%{_bindir}/veriT-SAT
%{_mandir}/man1/veriT.1*

%changelog
%autochangelog

Conclusion

I hope you learned something from this case study. Please send suggestions for improvements to Jerry James. If you want to submit the verit package to Fedora, please feel free. Just make sure nobody else beat you to it.