Blob Blame Raw
%global gitdate 20190702
%global commit  8a7a96bdf85bb43e613e26da842d21aa089c7b46
%global shortcommit %(c=%{commit}; echo ${c:0:7})

Name:           drat-trim
Version:        0
Release:        0.3.%{gitdate}.%{shortcommit}%{?dist}
Summary:        Proof checker for DIMACS proofs

License:        MIT
# Drat2er wants to use drat-trim as a library, but drat-trim only provides a
# binary.  Modify the sources to provide a library.
Patch0:         %{name}-library.patch
# Drat2er and CVC4 do not want to see commentary.  Apply a patch from the
# drat2er developers to optionally make it shut up.
Patch1:         %{name}-silent.patch

BuildRequires:  gcc
BuildRequires:  help2man

The proof checker DRAT-trim can be used to check whether a
propositional formula in the DIMACS format is unsatisfiable.  Given a
propositional formula and a clausal proof, DRAT-trim validates that the
proof is a certificate of unsatisfiability of the formula.  Clausal
proofs should be in the DRAT format which is used to validate the
results of the SAT competitions.

%package        devel
Summary:        Development files for %{name}
Requires:       %{name}%{?_isa} = %{version}-%{release}

%description    devel
Headers files and library links for developing applications that use

%package        tools
Summary:        Command line interface to %{name}
Requires:       %{name}%{?_isa} = %{version}-%{release}

%description    tools
This package contains a command line interface to %{name}.

%autosetup -p1 -n %{name}-%{commit}

# Build the library
gcc $RPM_OPT_FLAGS $RPM_LD_FLAGS -fPIC -shared -Wl,-h,lib%{name}.so.0 \
  -o lib%{name}.so.0.0.0 %{name}.c
ln -s lib%{name}.so.0.0.0 lib%{name}.so.0
ln -s lib%{name}.so.0 lib%{name}.so

# Build the command line interface
gcc $RPM_OPT_FLAGS $RPM_LD_FLAGS -o %{name} %{name}-main.c -L. -l%{name}

# Build the other tools
gcc $RPM_OPT_FLAGS $RPM_LD_FLAGS -o lrat-check lrat-check.c
gcc $RPM_OPT_FLAGS $RPM_LD_FLAGS -o to-clrat to-clrat.c

# Make man page for the command line interface
help2man --version-string=%{gitdate} -N -o %{name}.1 ./%{name}

# Install the library
mkdir -p %{buildroot}%{_libdir}
cp -a lib%{name}.so* %{buildroot}%{_libdir}

# Install the header file
mkdir -p %{buildroot}%{_includedir}
cp -p %{name}.h %{buildroot}%{_includedir}

# Install the binaries
mkdir -p %{buildroot}%{_bindir}
cp -p drat-trim lrat-check to-clrat %{buildroot}%{_bindir}

# Install the man page
mkdir -p %{buildroot}%{_mandir}/man1
cp -p drat-trim.1 %{buildroot}%{_mandir}/man1


%license LICENSE

%files          devel

%files          tools

* Wed Jul 24 2019 Fedora Release Engineering <> - 0-0.3.20190702.8a7a96b
- Rebuilt for

* Fri Jul 12 2019 Jerry James <> - 0-0.2.20190702.8a7a96b
- Bug fix for sortClause

* Thu Jun  6 2019 Jerry James <> - 0-0.1.20190516.e6fc615
- Initial RPM