# Upstream occasionally releases a subversion snapshot, but no "regular" # releases since the 0.1 release. %global svnver 1493 %global svntim 20120109svn Name: stp Version: 0.1 Release: 8.%{svntim}%{?dist} Summary: Constraint solver/decision procedure Group: Applications/Engineering License: MIT URL: http://sourceforge.net/projects/stp-fast-prover/ # The source for this package was pulled from upstream's subversion repository. # Use the following commands to generate the tarball: # # svn export -r %%{svnver} \ # https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp \ # stp-0.1 # tar cvJf stp-0.1.tar.xz stp-0.1 Source0: stp-%{version}.tar.xz # This patch has not yet been sent upstream. Fix a bunch of compiler warnings # that may indicate miscompiled code. Patch0: stp-warning.patch BuildRequires: bison BuildRequires: boost-devel BuildRequires: flex BuildRequires: valgrind BuildRequires: zlib-devel %description STP (Simple Theorem Prover) is a constraint solver (also referred to as a decision procedure or automated prover) aimed at solving constraints generated by program analysis tools, theorem provers, automated bug finders, intelligent fuzzers and model checkers. STP has been used in many research projects at Stanford, Berkeley, MIT, CMU and other universities, as well as companies and government agencies. The input to STP are formulas over the theory of bit-vectors and arrays (this theory captures most expressions from languages like C/C++/Java and Verilog), and the output of STP is a single bit of information that indicates whether the formula is satisfiable or not. If the input is satisfiable, then it also generates a variable assignment to satisfy the input formula. Additional information can be found at: http://people.csail.mit.edu/vganesh/STP_files/stp.html %package devel Summary: Development files for STP constraint solver/decision procedure Group: Applications/Engineering Requires: %{name}%{?_isa} = %{version}-%{release} Provides: %{name}-static = %{version}-%{release} # This "devel" package provides a static (not dynamic) library because: # 1. This is the normal usage mode when linking this as a library; # it's what upstream and existing programs that use this program expect. # 2. This speeds execution. In this library, speed matters. # There's a speed penalty for .so files, and this program is much # like a chess program - it's essentially an inner loop that searches # a massive space of possibilities. # A dynamic .so version could be create using: # gcc -shared -Wl,-soname,libstp.so.1 -o libstp.so.1.0.1 libstp.a # but this would require -fpic to compile (slowing the results). # See my document: # http://www.dwheeler.com/program-library/Program-Library-HOWTO/ %description devel Development files for the STP (Simple Theorem Prover), a constraint solver (also referred to as a decision procedure or automated prover). Provides a static library. %prep %setup -q %patch0 # Make sure nothing uses the shipped boost sources rm -fr src/boost # We do not want to know about the order of member initializers sed -i "s/\(-Wno-deprecated\)/\1 -Wno-reorder/" scripts/Makefile.common # Avoid a BR on subversion, as well as subversion version hell sed -i "s|\`svnversion \$(TOP)\`|%{svnver}|" src/main/Makefile %build scripts/configure --with-prefix=%{_prefix} # DO NOT use _smp_mflags; build will fail. make %{?_smp_mflags} all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir} %check make regressall %install mkdir -p %{buildroot}%{_bindir} mkdir -p %{buildroot}%{_includedir}/stp mkdir -p %{buildroot}%{_libdir} # This "make install" doesn't support DESTDIR=%%{buildroot}. # We'll rig PREFIX/LIB_DIR, since that happens to work for this makefile. make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir} %files %{_bindir}/* %doc AUTHORS README LICENSE LICENSE_COMPONENTS papers %files devel %{_libdir}/libstp*.a %{_includedir}/stp/ %changelog * Tue Jan 10 2012 Jerry James - 0.1-8.20120109svn - Update to recent subversion snapshot * Tue Dec 13 2011 Jerry James - 0.1-7.20111130svn - Update to recent subversion snapshot - Minor spec file cleanups * Wed Feb 09 2011 Fedora Release Engineering - 0.1-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild * Sun Jul 26 2009 Fedora Release Engineering - 0.1-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild * Mon Mar 6 2009 David A. Wheeler 0.1-4 - Re-sync with CVS * Mon Mar 6 2009 David A. Wheeler 0.1-3 - Modified spec so can rebuild in proper order on Fedora * Mon Mar 3 2009 David A. Wheeler 0.1-2 - Fixed comments by Marcela Maslanova, mmaslano (at) redhat*DOT*com 2009-02-26 - Moved definitions of subpackages to "top" of spec before prep. - moved "check" before "files". - Use macro for release version 0.1-11-18-2008 for future updates. - No doc for -devel package; it's already in the base. - CPPFLAGS now includes optflags. * Mon Feb 23 2009 David A. Wheeler 0.1-1 - Initial packaging