diff --git a/.gitignore b/.gitignore index 006045d..e63ff09 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ /rel-06w.tar.gz +/sr19.tar.gz diff --git a/cadical-shared.patch b/cadical-shared.patch index ba908ca..a14f301 100644 --- a/cadical-shared.patch +++ b/cadical-shared.patch @@ -1,28 +1,38 @@ ---- makefile.in.orig 2018-03-10 07:22:11.000000000 -0700 -+++ makefile.in 2018-07-06 13:26:02.288756528 -0600 -@@ -8,12 +8,17 @@ BUILD=../$(shell pwd|sed -e 's,.*/,,') - CXX=@CXX@ - CXXFLAGS=@CXXFLAGS@ - COMPILE=$(CXX) $(CXXFLAGS) -I$(BUILD) --all: cadical libcadical.a -+all: cadical libcadical.so - %.o: ../src/%.cpp - $(COMPILE) -c $< - -include dependencies --cadical: main.o app.o libcadical.a makefile -+cadical: main.o app.o libcadical.so makefile - $(COMPILE) -o $@ main.o app.o -L. -lcadical +--- makefile.in.orig 2019-06-06 00:37:51.000000000 -0600 ++++ makefile.in 2019-06-06 09:48:06.184149590 -0600 +@@ -25,7 +25,7 @@ COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR) + + #--------------------------------------------------------------------------# + +-all: libcadical.a cadical mobical ++all: libcadical.so cadical mobical + + #--------------------------------------------------------------------------# + +@@ -39,12 +39,18 @@ all: libcadical.a cadical mobical + # Application binaries (the stand alone solver 'cadical' and the model based + # tester 'mobical') and the library are the main build targets. + +-cadical: cadical.o libcadical.a makefile ++cadical: cadical.o libcadical.so makefile + $(COMPILE) -o $@ $< -L. -lcadical + +-mobical: mobical.o libcadical.a makefile ++mobical: mobical.o libcadical.so makefile + $(COMPILE) -o $@ $< -L. -lcadical + +libcadical.so: $(OBJ) makefile + rm -f $@ + $(COMPILE) -shared -Wl,-h,libcadical.so.0 -o libcadical.so.0.0.0 $(OBJ) + ln -s libcadical.so.0.0.0 libcadical.so.0 + ln -s libcadical.so.0 $@ ++ libcadical.a: $(OBJ) makefile - rm -f $@ ar rc $@ $(OBJ) ---- test/run-api-tests.sh.orig 2018-03-10 07:22:11.000000000 -0700 -+++ test/run-api-tests.sh 2018-07-06 13:33:14.157429018 -0600 -@@ -16,10 +16,10 @@ msg () { + +--- test/api/run.sh.orig 2019-06-06 00:37:51.000000000 -0600 ++++ test/api/run.sh 2019-06-06 09:48:52.553322222 -0600 +@@ -28,8 +28,8 @@ die "needs to be called from a top-level [ -f "$CADICALBUILD/makefile" ] || \ die "can not find '$CADICALBUILD/makefile' (run 'configure' first)" @@ -31,8 +41,5 @@ +[ -f "$CADICALBUILD/libcadical.so" ] || \ + die "can not find '$CADICALBUILD/libcadical.so' (run 'make' first)" --msg "API testing '$CADICALBUILD/libcadical.a'" -+msg "API testing '$CADICALBUILD/libcadical.so'" - - CXX=`grep '^CXX=' "$CADICALBUILD/makefile"|sed -e 's,CXX=,,'` - + echo -n "$HILITE" + echo "---------------------------------------------------------" diff --git a/cadical-vector.patch b/cadical-vector.patch deleted file mode 100644 index b9962c2..0000000 --- a/cadical-vector.patch +++ /dev/null @@ -1,30 +0,0 @@ ---- src/analyze.cpp.orig 2018-03-10 07:22:11.000000000 -0700 -+++ src/analyze.cpp 2018-07-06 09:56:56.466164260 -0600 -@@ -186,7 +186,8 @@ void Internal::clear_seen () { - - void Internal::clear_levels () { - for (const_int_iterator i = levels.begin (); i != levels.end (); i++) -- control[*i].reset (); -+ if (*i < control.size()) -+ control[*i].reset (); - levels.clear (); - } - ---- src/elim.cpp.orig 2018-03-10 07:22:11.000000000 -0700 -+++ src/elim.cpp 2018-07-06 10:19:12.034202168 -0600 -@@ -165,6 +165,7 @@ bool Internal::resolve_clauses (Clause * - - unmark (c); - const size_t size = clause.size (); -+ const int unit = (size == 0) ? 0 : clause[0]; - if (tautological || satisfied || eliminated || size <= 1) clause.clear (); - - assert (!eliminated); -@@ -192,7 +193,6 @@ bool Internal::resolve_clauses (Clause * - LOG ("empty resolvent"); - learn_empty_clause (); - } else if (size == 1) { -- const int unit = clause[0]; - LOG ("unit resolvent %d", unit); - assign_unit (unit); - } else LOG (clause, "resolvent"); diff --git a/cadical.spec b/cadical.spec index 7a75e5f..d8eb65b 100644 --- a/cadical.spec +++ b/cadical.spec @@ -1,20 +1,29 @@ +# I do not understand upstream's versioning scheme. Starting with version +# sr19, we revert to version 0 and use the release field to enforce proper +# update ordering. +%global upver sr19 + Name: cadical -Version: 06w -Release: 3%{?dist} +Version: 0 +Release: 1.%{upver}%{?dist} Summary: Simplified SAT solver License: MIT URL: http://fmv.jku.at/cadical/ -Source0: https://github.com/arminbiere/%{name}/archive/rel-%{version}.tar.gz +Source0: https://github.com/arminbiere/%{name}/archive/%{upver}.tar.gz # Fedora-only patch: build a shared library instead of a static library Patch0: %{name}-shared.patch -# Patch to be sent upstream: fix out-of-bounds vector accesses -Patch1: %{name}-vector.patch -BuildRequires: drabt +BuildRequires: drat-trim-tools BuildRequires: gcc-c++ +BuildRequires: glibc-langpack-en +BuildRequires: help2man +BuildRequires: zlib-devel Requires: %{name}-libs%{?_isa} = %{version}-%{release} +# This can be removed when Fedora 30 reaches EOL +Obsoletes: cadical = 06w + %description CaDiCaL is a simplified Satisfiability solver. The goal of the development of CaDiCaL is to obtain a CDCL solver, which is easy to @@ -37,26 +46,28 @@ Library links and header files for developing applications that use %{name}. %prep -%autosetup -p0 -n %{name}-rel-%{version} +%autosetup -p0 -n %{name}-%{upver} # We have commas in optflags, so commas can't be used as sed delimiters in -# the configure script. -sed -i '/^-e/s/,/|/g' configure - -# Fix build flags in the tests -sed -i 's|-g|%{optflags}|' test/run-api-tests.sh +# the configure script. Also, do not override our build flags. +sed -i '/^-e/s/,/|/g;s/-O3/-O2/' configure %build # The configure script is NOT generated by autoconf. Do NOT use the # %%configure macro here. -CXXFLAGS="%{optflags} -fPIC" ./configure --no-realloc +CXXFLAGS="%{optflags} -fPIC" ./configure %make_build +# Make man pages for the command line interface +export LD_LIBRARY_PATH=$PWD/build +help2man --version-string=%{upver} -N -o cadical.1 build/cadical +help2man --version-string=%{upver} -N -o mobical.1 -h -h build/mobical + %install # The makefile has no install target. Install by hand. -# Install the binary +# Install the binaries mkdir -p %{buildroot}%{_bindir} -cp -p build/cadical %{buildroot}%{_bindir} +cp -p build/{cad,mob}ical %{buildroot}%{_bindir} # Install the library mkdir -p %{buildroot}%{_libdir} @@ -68,23 +79,43 @@ ln -s libcadical.so.0 %{buildroot}%{_libdir}/libcadical.so mkdir -p %{buildroot}%{_includedir} cp -p src/cadical.hpp %{buildroot}%{_includedir} +# Install the man pages +mkdir -p %{buildroot}%{_mandir}/man1 +cp -p *.1 %{buildroot}%{_mandir}/man1 + %check +# Prevent rebuilding the library while testing +sed -i '/make -C \$CADICALBUILD/d;/^make$/d' test/*/run.sh + +# Some mobical tests randomly fail due to exceeding time or memory limits. +# Turn those tests off. +sed -i 's/ mbt$//' test/makefile + export LD_LIBRARY_PATH=$PWD/build -make test +make -C test %files -%{_bindir}/%{name} +%{_bindir}/cadical +%{_bindir}/mobical +%{_mandir}/man1/cadical.1* +%{_mandir}/man1/mobical.1* %files libs %license LICENSE %doc CONTRIBUTING README.md -%{_libdir}/lib%{name}.so.* +%{_libdir}/lib%{name}.so.0* %files devel %{_includedir}/%{name}.hpp %{_libdir}/lib%{name}.so %changelog +* Wed Jun 12 2019 Jerry James - 0-1.sr19 +- New upstream version +- Adapt to upstream version scheme +- Drop upstreamed -vector patch +- Add man pages + * Thu Jan 31 2019 Fedora Release Engineering - 06w-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild diff --git a/sources b/sources index 3be7a35..cdd427f 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (rel-06w.tar.gz) = 344962411e4e527b8b247cefc8d87f55e1ad4dcc6fa48e57ceb174d1f90b689341cc81d80a49fbe3a02d7856e18b478c3876fe78abec357565b67be31e891b86 +SHA512 (sr19.tar.gz) = e6655562dd9d6344d2e292bff4d199d1d2d3ec69e21338294a5347338e7fcfd2896e4dc800ddd6bc35019499a867053cb1d4dccd02ce4e8ca6531f4c4665ce98