Name:           vampire
Version:        5.0.1
Release:        1%{?dist}
Summary:        Automated theorem prover for first-order logic

License:        BSD-3-Clause
URL:            https://vprover.github.io/
# The GitHub release tarball ships the cadical and viras submodules empty, but
# CMake requires both. Source0 is a complete tree regenerated as follows (the
# optional z3 submodule is omitted, so Vampire builds without SMT support):
#   git clone --branch v%{version} --depth 1 \
#       https://github.com/vprover/vampire vampire-%{version}
#   cd vampire-%{version}
#   git submodule update --init --depth 1 cadical viras
#   rm -rf .git */.git z3
#   cd .. && tar czf vampire-%{version}.tar.gz vampire-%{version}
Source0:        vampire-%{version}.tar.gz

BuildRequires:  cmake
BuildRequires:  gcc-c++
BuildRequires:  make
# Generate a man page from --help (upstream ships none).
BuildRequires:  help2man

# Bundled in-tree by upstream. Built without Z3, so there is no SMT support.
# TODO(Fedora): unbundle mini-gmp -> system gmp; evaluate the system CaDiCaL.
Provides:       bundled(cadical)
Provides:       bundled(minisat)
Provides:       bundled(mini-gmp) = 6.3.0
Provides:       bundled(viras)

%description
Vampire is an automated theorem prover for first-order classical logic. It has
repeatedly won the CASC competition (the "world cup for theorem provers") and
is widely used to discharge proof obligations, including as an automated
backend for interactive proof assistants. This build is compiled without Z3,
so SMT support is disabled.

%prep
%autosetup -n %{name}-%{version}

%build
%cmake
# Build only the prover itself, not the bundled unit-test / subsat executables.
%cmake_build --target vampire

%install
%cmake_install

# Man page generated from the binary's --help (upstream ships none).
help2man --no-info --no-discard-stderr --section 1 \
    --name 'automated theorem prover for first-order logic' \
    %{buildroot}%{_bindir}/vampire > vampire.1
install -Dpm0644 vampire.1 %{buildroot}%{_mandir}/man1/vampire.1

%files
%license LICENCE
%doc README.md AUTHORS THANKS
%{_bindir}/vampire
%{_mandir}/man1/vampire.1*

%changelog
* Wed Jun 24 2026 Morgan Hough <morgan.hough@gmail.com> - 5.0.1-1
- Initial package (first-order theorem prover), built without Z3/SMT