cvc4/cvc4.spec

366 lines
13 KiB
RPMSpec
Raw Normal View History

# CVC4 1.4 and later need a modified glpk, unavailable in Fedora. Therefore,
# we currently build without glpk support.
2014-02-03 14:53:17 +00:00
Name: cvc4
2018-07-11 03:22:52 +00:00
Version: 1.6
2018-11-27 04:13:16 +00:00
Release: 3%{?dist}
2014-02-03 14:53:17 +00:00
Summary: Automatic theorem prover for SMT problems
# License breakdown:
# - Files containing code under the Boost license:
# o src/util/channel.h
# o examples/hashsmt/sha1.hpp
# - Files containing code under the BSD license:
# o src/parser/antlr_input_imports.cpp
# o src/parser/bounded_token_buffer.cpp
# - All other files are distributed under the MIT license
2018-07-11 03:22:52 +00:00
License: Boost and BSD and MIT
2017-01-28 19:32:18 +00:00
URL: http://cvc4.cs.stanford.edu/
Source0: http://cvc4.cs.stanford.edu/downloads/builds/src/%{name}-%{version}.tar.gz
2014-02-03 14:53:17 +00:00
# Fix some doxygen problems. Upstream plans to fix this differently.
Patch0: %{name}-doxygen.patch
# Fix various autoconf problems
2018-07-11 03:22:52 +00:00
Patch1: %{name}-autoconf.patch
# Fix detection of cadical
Patch2: %{name}-cadical.patch
# Fix detection of symfpu
Patch3: %{name}-symfpu.patch
# Fix out-of-bounds vector accesses
Patch4: %{name}-vec.patch
2014-02-03 14:53:17 +00:00
BuildRequires: abc-devel
2014-02-03 14:53:17 +00:00
BuildRequires: antlr3-C-devel
BuildRequires: antlr3-tool
BuildRequires: boost-devel
2018-07-11 03:22:52 +00:00
BuildRequires: cadical-devel
2014-02-03 14:53:17 +00:00
BuildRequires: chrpath
2018-07-11 03:22:52 +00:00
BuildRequires: cryptominisat-devel
2014-02-03 14:53:17 +00:00
BuildRequires: cxxtest
BuildRequires: doxygen-latex
2017-01-28 19:32:18 +00:00
BuildRequires: gcc-c++
BuildRequires: ghostscript
2014-02-03 14:53:17 +00:00
BuildRequires: gmp-devel
BuildRequires: java-devel
2014-02-03 14:53:17 +00:00
BuildRequires: jpackage-utils
2018-07-11 03:22:52 +00:00
BuildRequires: lfsc-devel
BuildRequires: libtool
BuildRequires: perl-interpreter
2017-01-28 19:32:18 +00:00
BuildRequires: python2
2014-02-03 14:53:17 +00:00
BuildRequires: readline-devel
BuildRequires: swig
2018-07-11 03:22:52 +00:00
BuildRequires: symfpu-devel
2014-02-03 14:53:17 +00:00
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
2014-02-03 14:53:17 +00:00
%description
CVC4 is an efficient open-source automatic theorem prover for
satisfiability modulo theories (SMT) problems. It can be used to prove
the validity (or, dually, the satisfiability) of first-order formulas in
a large number of built-in logical theories and their combination.
CVC4 is the fourth in the Cooperating Validity Checker family of tools
(CVC, CVC Lite, CVC3) but does not directly incorporate code from any
previous version. A joint project of NYU and U Iowa, CVC4 aims to
support the features of CVC3 and SMT-LIBv2 while optimizing the design
of the core system architecture and decision procedures to take
advantage of recent engineering and algorithmic advances.
CVC4 is intended to be an open and extensible SMT engine, and it can be
used as a stand-alone tool or as a library, with essentially no limit on
its use for research or commercial purposes.
%package devel
Summary: Headers and other files for developing with %{name}
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
%description devel
Header files and library links for developing applications that use %{name}.
%package doc
Summary: Interface documentation for %{name}
Provides: bundled(jquery)
2014-02-03 14:53:17 +00:00
%description doc
Interface documentation for %{name}.
%package libs
Summary: Library containing an automatic theorem prover for SMT problems
%description libs
Library containing the core of the %{name} automatic theorem prover for
SMT problems.
%package java
Summary: Java interface to %{name}
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
Requires: java-headless
Requires: jpackage-utils
%description java
Java interface to %{name}.
%prep
2018-07-11 03:22:52 +00:00
%autosetup -p0
2014-02-03 14:53:17 +00:00
2018-07-11 03:22:52 +00:00
# Regenerate configure due to patch 1
autoreconf -fi
# Do not override Fedora's optimization settings
sed -i 's/-O3/-O2/' \
src/prop/minisat/mtl/template.mk src/prop/minisat/Makefile \
src/prop/bvminisat/mtl/template.mk src/prop/bvminisat/Makefile
# Avoid hardcoded rpaths and allow boost to use g++ 5.0 and higher.
sed -e 's,^hardcode_libdir_flag_spec=.*,hardcode_libdir_flag_spec="",g' \
-e 's,runpath_var=LD_RUN_PATH,runpath_var=DIE_RPATH_DIE,g' \
-e 's,OPTLEVEL=3,OPTLEVEL=2,g' \
-e '/gcc48/i\ "defined __GNUC__ && __GNUC__ == 8 && !defined __ICC @ gcc80" \\\n "defined __GNUC__ && __GNUC__ == 7 && !defined __ICC @ gcc70" \\\n "defined __GNUC__ && __GNUC__ == 6 && !defined __ICC @ gcc60" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 3 && !defined __ICC @ gcc53" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 2 && !defined __ICC @ gcc52" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 1 && !defined __ICC @ gcc51" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 0 && !defined __ICC @ gcc50" \\' \
2014-02-03 14:53:17 +00:00
-i configure
2017-03-03 19:09:26 +00:00
# Change the Java installation paths for Fedora and fix FTBFS
sed -e "s|^\(javalibdir =.*\)jni|\1java/%{name}|" \
-e 's/ -Wno-all//' \
-i src/bindings/Makefile.am
sed -e "s|^\(javalibdir =.*\)jni|\1java/%{name}|" \
-e 's/ -Wno-all//' \
-i src/bindings/Makefile.in
2014-02-03 14:53:17 +00:00
# Fix access to an uninitialized variable
sed -e 's/Kind k;/Kind k = kind::UNDEFINED_KIND;/' \
-i src/parser/cvc/CvcParser.c
# Help the documentation generator
cp -p COPYING src/bindings/compat/c
# Preserve timestamps when installing
for fil in $(find . -name Makefile\*); do
sed -i 's/$(install_sh) -c/$(install_sh) -p/' $fil
done
# Fix an include path in the tests
sed -i 's,@CXXTEST@,%{_includedir}/cxxtest,' test/unit/Makefile.am
2014-02-03 14:53:17 +00:00
%build
export CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc"
2018-07-11 03:22:52 +00:00
if [ "%{__isa_bits}" = "64" ]; then
CPPFLAGS+=" -DLIN64"
else
CPPFLAGS+=" -DLIN"
fi
export CFLAGS="%{optflags} -fsigned-char"
export CXXFLAGS="%{optflags} -fsigned-char"
%configure --enable-gpl --enable-proof --enable-language-bindings=all \
2018-07-11 03:22:52 +00:00
--disable-silent-rules --with-portfolio --without-compat \
--with-abc --with-abc-dir=%{_prefix} \
--with-cadical --with-cadical-dir=%{_prefix} \
--with-cryptominisat --with-cryptominisat-dir=%{_prefix} \
--with-lfsc --with-lfsc-dir=%{_prefix} \
--with-symfpu --with-symfpu-dir=%{_prefix} \
--with-readline
2014-02-03 14:53:17 +00:00
# Workaround libtool reordering -Wl,--as-needed after all the libraries
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
sed -i 's/CC=.g../& -Wl,--as-needed/' $BUILDS/libtool
2014-02-03 14:53:17 +00:00
make %{?_smp_mflags}
make doc
%install
%make_install
# Remove unwanted libtool files
find %{buildroot}%{_libdir} -name \*.la | xargs rm -f
# Remove empty directories for language bindings that do not yet exist
rm -fr %{buildroot}%{_libdir}/{csharp,ocaml,perl5,php,pyshared,ruby,tcltk}
rm -fr %{buildroot}%{_datadir}/{csharp,perl5,php,pyshared}
# Make the Java installation match Fedora requirements
if [ "%{_libdir}/java" != "%{_jnidir}" ]; then
mkdir -p %{buildroot}%{_jnidir}
mv %{buildroot}%{_libdir}/java/cvc4 %{buildroot}%{_jnidir}
rmdir %{buildroot}%{_libdir}/java
fi
# Remove still more hardcoded rpaths
chrpath -d %{buildroot}%{_bindir}/* \
%{buildroot}%{_libdir}/lib%{name}*.so.*.*.* \
%{buildroot}%{_jnidir}/%{name}/lib%{name}*.so.*.*.*
# Help the debuginfo generator
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
2014-02-03 14:53:17 +00:00
for dir in decision expr main parser printer prop smt theory theory/arith \
theory/arrays theory/booleans theory/bv theory/datatypes theory/idl \
theory/quantifiers theory/rewriterules theory/strings theory/uf; do
ln -s $PWD/src/$dir/options $BUILDS/src/$dir
2014-02-03 14:53:17 +00:00
done
ln -s production-abc-proof/src $BUILDS/../src
ln -s $PWD/src/options/base_options $BUILDS/src/options
2014-02-03 14:53:17 +00:00
ln -s $PWD/src/options/base_options_template.cpp $BUILDS/src/options
ln -s $PWD/src/options/options_holder_template.h $BUILDS/src/options
ln -s $PWD/src/options/options_template.cpp $BUILDS/src/options
ln -s $PWD/src/smt/smt_options_template.cpp $BUILDS/src/smt
2018-05-31 01:29:50 +00:00
%ldconfig_scriptlets libs
2014-02-03 14:53:17 +00:00
%check
# The tests use a large amount of stack space
ulimit -s unlimited
# Do not rebuild when checking
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
sed -e 's/\(units.*:\) all/\1/' \
-e 's/\(regress.*:\) all/\1/' \
-i $BUILDS/Makefile $BUILDS/Makefile.builds
# Fix bad include paths in the test code
sed 's,/barrett/scratch.*/expr/,./,' \
test/unit/expr/expr_manager_public.cpp \
test/unit/expr/expr_public.cpp \
test/unit/expr/type_cardinality_public.cpp
# Fix the Java test's access to the JNI object it needs
sed 's,loadLibrary("cvc4jni"),load("%{buildroot}%{_jnidir}/%{name}/libcvc4jni.so"),' \
-i test/system/CVC4JavaTest.java
export LD_LIBRARY_PATH=%{buildroot}%{_libdir}
2014-02-03 14:53:17 +00:00
make check
%files
2018-07-11 03:22:52 +00:00
%doc AUTHORS NEWS README RELEASE-NOTES THANKS
2014-02-03 14:53:17 +00:00
%{_bindir}/*
%{_datadir}/%{name}/
2014-02-03 14:53:17 +00:00
%{_mandir}/man1/*
%{_mandir}/man5/*
%files doc
2018-07-11 03:22:52 +00:00
%license COPYING
2014-02-03 14:53:17 +00:00
%doc doc/doxygen/*
%files libs
%license COPYING
2014-02-03 14:53:17 +00:00
%{_libdir}/lib%{name}*.so.*
%files devel
%{_includedir}/%{name}/
%{_libdir}/lib%{name}*.so
%{_mandir}/man3/*
%files java
%{_javadir}/*.jar
%{_jnidir}/%{name}/
%changelog
2018-11-27 04:13:16 +00:00
* Mon Nov 26 2018 Jerry James <loganjerry@gmail.com> - 1.6-3
- Rebuild for updated abc
* Thu Jul 12 2018 Fedora Release Engineering <releng@fedoraproject.org> - 1.6-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
2018-07-11 03:22:52 +00:00
* Tue Jul 10 2018 Jerry James <loganjerry@gmail.com> - 1.6-1
- New upstream release
* Wed Feb 07 2018 Fedora Release Engineering <releng@fedoraproject.org> - 1.5-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
* Thu Feb 1 2018 Jerry James <loganjerry@gmail.com> - 1.5-5
- Fix FTBFS with automake 1.5.1 (bz 1482152)
* Wed Aug 02 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.5-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
* Wed Jul 26 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.5-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
2017-07-21 07:44:14 +00:00
* Fri Jul 21 2017 Kalev Lember <klember@redhat.com> - 1.5-2
- Rebuilt for Boost 1.64
* Sat Jul 15 2017 Jerry James <loganjerry@gmail.com> - 1.5-1
- New upstream release
- Drop upstreamed patches: -signed, -boolean, -minisat
- Add -constant patch to fix undefined symbols in the JNI shared object
- Add cryptominisat4 support
* Mon May 15 2017 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.4-15
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_27_Mass_Rebuild
2017-03-03 19:09:26 +00:00
* Fri Mar 3 2017 Jerry James <loganjerry@gmail.com> - 1.4-14
- Fix FTBFS (bz 1427891)
2017-02-07 13:27:33 +00:00
* Tue Feb 07 2017 Kalev Lember <klember@redhat.com> - 1.4-13
- Rebuilt for Boost 1.63
* Thu Jan 12 2017 Igor Gnatenko <ignatenko@redhat.com> - 1.4-12
- Rebuild for readline 7.x
* Tue May 17 2016 Jonathan Wakely <jwakely@redhat.com> - 1.4-11
- Rebuilt for linker errors in boost (#1331983)
* Wed Feb 03 2016 Fedora Release Engineering <releng@fedoraproject.org> - 1.4-10
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
2016-01-15 04:12:35 +00:00
* Fri Jan 15 2016 Jonathan Wakely <jwakely@redhat.com> - 1.4-9
- Rebuilt for Boost 1.60
2015-08-27 20:20:58 +00:00
* Thu Aug 27 2015 Jonathan Wakely <jwakely@redhat.com> - 1.4-8
- Rebuilt for Boost 1.59
* Wed Jul 29 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.4-7
- Rebuilt for https://fedoraproject.org/wiki/Changes/F23Boost159
2015-07-22 16:20:37 +00:00
* Wed Jul 22 2015 David Tardon <dtardon@redhat.com> - 1.4-6
- rebuild for Boost 1.58
* Wed Jun 17 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.4-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
2015-05-02 11:16:06 +00:00
* Sat May 02 2015 Kalev Lember <kalevlember@gmail.com> - 1.4-4
- Rebuilt for GCC 5 C++11 ABI change
* Fri Mar 20 2015 Jerry James <loganjerry@gmail.com> - 1.4-3
- Don't use perftools at all due to random weirdness on multiple platforms
- Also Obsoletes/Provides lfsc-devel
* Wed Mar 11 2015 Jerry James <loganjerry@gmail.com> - 1.4-2
- Add -boolean, -minisat, and -signed patches to fix test failures
- Fix boost detection with g++ 5.0
- Fix access to an uninitialized variable
- Help the documentation generator find COPYING
- Build with -fsigned-char to fix the arm build
- Prevent rebuilds while running checks
- Remove i686 from have_perftools due to test failures
2015-01-27 03:04:04 +00:00
* Tue Jan 27 2015 Petr Machata <pmachata@redhat.com> - 1.4-2
- Rebuild for boost 1.57.0
* Thu Jan 1 2015 Jerry James <loganjerry@gmail.com> - 1.4-1
- New upstream release
- Drop updated test files, now included upstream
- Drop obsolete workarounds for glpk compatibility
- Drop lfsc BR/R, as it has been incorporated into cvc4
* Fri Aug 22 2014 Jerry James <loganjerry@gmail.com> - 1.3-7
- Remove arm platforms from have_perftools due to bz 1109309
* Sat Aug 16 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.3-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
* Sat Jun 07 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.3-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
2014-05-23 08:56:30 +00:00
* Fri May 23 2014 David Tardon <dtardon@redhat.com> - 1.3-5
- rebuild for boost 1.55.0
* Thu Mar 6 2014 Jerry James <loganjerry@gmail.com> - 1.3-4
- Merge changes from Dan Horák to fix secondary arch builds
* Tue Feb 4 2014 Jerry James <loganjerry@gmail.com> - 1.3-3
- glibc Provides /sbin/ldconfig, not /usr/sbin/ldconfig
2014-02-03 14:53:17 +00:00
* Mon Jan 27 2014 Jerry James <loganjerry@gmail.com> - 1.3-2
- Install JNI objects in %%{_jnidir}
- The documentation is arch-specific after all
2014-02-03 14:53:17 +00:00
* Wed Jan 22 2014 Jerry James <loganjerry@gmail.com> - 1.3-1
- Initial RPM