cpet/openbsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update to latest git master.

Browse Source 
Built with cmake, installs minisat libraries (needed for a devel/stp
update).  Discussed with jasper@ at t2k17.
This commit is contained in:
jca 2017-08-20 16:39:44 +00:00
parent be05572271
commit d7d6ed1300
10 changed files with 69 additions and 156 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
math/minisat/Makefile
View File

@ -1,9 +1,14 @@
# $OpenBSD: Makefile,v 1.12 2017/07/26 22:45:26 sthen Exp $
# $OpenBSD: Makefile,v 1.13 2017/08/20 16:39:44 jca Exp $
COMMENT= minimalistic Boolean satisfiability solver
DISTNAME= minisat-2.2.0
REVISION = 2
DISTNAME= minisat-2.2.0.20170810
GH_ACCOUNT= niklasso
GH_PROJECT= minisat
GH_COMMIT= 37dc6c67e2af26379d88ce349eb9c4c6160e8543
SHARED_LIBS += minisat 0.0 # 2.1
CATEGORIES= math
HOMEPAGE= http://minisat.se/
@ -13,28 +18,10 @@ MAINTAINER= Jasper Lievisse Adriaanse <jasper@openbsd.org>
# MIT
PERMIT_PACKAGE_CDROM= Yes
MASTER_SITES= ${HOMEPAGE}downloads/
DISTFILES= ${DISTNAME}${EXTRACT_SUFX} \
MiniSat.pdf
EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX}
WANTLIB += c m ${COMPILER_LIBCXX} z
USE_GMAKE= Yes
ALL_TARGET= minisat
MODULES= devel/cmake
NO_TEST= Yes
MAKE_FLAGS= CXX="${CXX}"
MAKE_ENV+= MROOT=${WRKBUILD}
WRKDIST= ${WRKDIR}/minisat
do-build:
cd ${WRKBUILD}/core && ${MAKE_ENV} ${MAKE_PROGRAM} ${MAKE_FLAGS}
cd ${WRKBUILD}/simp && ${MAKE_ENV} ${MAKE_PROGRAM} ${MAKE_FLAGS}
do-install:
${INSTALL_PROGRAM} ${WRKSRC}/core/minisat ${PREFIX}/bin/minisat
${INSTALL_PROGRAM} ${WRKSRC}/simp/minisat ${PREFIX}/bin/minisats
${INSTALL_DATA_DIR} ${PREFIX}/share/doc/minisat
${INSTALL_DATA} ${DISTDIR}/MiniSat.pdf ${PREFIX}/share/doc/minisat
.include <bsd.port.mk>

6
math/minisat/distinfo
View File

@ -1,4 +1,2 @@
SHA256 (MiniSat.pdf) = Uxl9vXg8kkomJ9deMFcGKXmISUJlvV5eyHOEDl15esQ=
SHA256 (minisat-2.2.0.tar.gz) = kpV9hRzcO63f4HtfyA7VoCN8SJ0MUq5y9ihEs7RteAg=
SIZE (MiniSat.pdf) = 327416
SIZE (minisat-2.2.0.tar.gz) = 43879
SHA256 (minisat-2.2.0.20170810-37dc6c67.tar.gz) = PbBbAvkcSwl7eWLlIyJapeb6mmwNQnBKFwsBsGnN/P4=
SIZE (minisat-2.2.0.20170810-37dc6c67.tar.gz) = 49544

19
math/minisat/patches/patch-core_Main_cc
View File

@ -1,19 +0,0 @@
$OpenBSD: patch-core_Main_cc,v 1.1 2010/08/19 14:19:22 edd Exp $
OpenBSD has no RLIMIT_AS
--- core/Main.cc.orig Thu Aug 19 14:33:12 2010
+++ core/Main.cc Thu Aug 19 14:34:39 2010
@@ -112,10 +112,10 @@ int main(int argc, char** argv)
if (mem_lim != INT32_MAX){
rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
rlimit rl;
- getrlimit(RLIMIT_AS, &rl);
+ getrlimit(RLIMIT_DATA, &rl);
if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
rl.rlim_cur = new_mem_lim;
- if (setrlimit(RLIMIT_AS, &rl) == -1)
+ if (setrlimit(RLIMIT_DATA, &rl) == -1)
printf("WARNING! Could not set resource limit: Virtual memory.\n");
} }

12
math/minisat/patches/patch-core_SolverTypes_h → math/minisat/patches/patch-minisat_core_SolverTypes_h
View File

@ -1,9 +1,9 @@
$OpenBSD: patch-core_SolverTypes_h,v 1.1 2017/05/19 23:20:59 espie Exp $
$OpenBSD: patch-minisat_core_SolverTypes_h,v 1.1 2017/08/20 16:39:44 jca Exp $
Index: core/SolverTypes.h
--- core/SolverTypes.h.orig
+++ core/SolverTypes.h
@@ -47,7 +47,7 @@ struct Lit {
Index: minisat/core/SolverTypes.h
--- minisat/core/SolverTypes.h.orig
+++ minisat/core/SolverTypes.h
@@ -52,7 +52,7 @@ struct Lit {
int x;
// Use this as a constructor:
@ -12,7 +12,7 @@ Index: core/SolverTypes.h
bool operator == (Lit p) const { return x == p.x; }
bool operator != (Lit p) const { return x != p.x; }
@@ -55,7 +55,7 @@ struct Lit {
@@ -60,7 +60,7 @@ struct Lit {
};

21
math/minisat/patches/patch-minisat_utils_System_cc Normal file
View File

@ -0,0 +1,21 @@
$OpenBSD: patch-minisat_utils_System_cc,v 1.1 2017/08/20 16:39:44 jca Exp $
Index: minisat/utils/System.cc
--- minisat/utils/System.cc.orig
+++ minisat/utils/System.cc
@@ -71,13 +71,13 @@ double Minisat::memUsedPeak(bool strictlyPeak) {
double peak = memReadPeak() / (double)1024;
return peak == 0 && !strictlyPeak ? memUsed() : peak; }
-#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__)
+#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__OpenBSD__) || defined(__gnu_hurd__)
double Minisat::memUsed() {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
return (double)ru.ru_maxrss / 1024; }
-double Minisat::memUsedPeak() { return memUsed(); }
+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
#elif defined(__APPLE__)

55
math/minisat/patches/patch-mtl_template_mk
View File

@ -1,55 +0,0 @@
$OpenBSD: patch-mtl_template_mk,v 1.1 2010/08/19 14:19:22 edd Exp $
Print compiler options and remove OTT optimisation
--- mtl/template.mk.orig Sat Jul 10 17:07:36 2010
+++ mtl/template.mk Tue Jul 13 14:14:42 2010
@@ -22,7 +22,7 @@ CXX ?= g++
CFLAGS ?= -Wall -Wno-parentheses
LFLAGS ?= -Wall
-COPTIMIZE ?= -O3
+#COPTIMIZE ?= -O3
CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
LFLAGS += -lz
@@ -41,13 +41,13 @@ libd: lib$(LIB)_debug.a
libr: lib$(LIB)_release.a
## Compile options
-%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG
+%.o: CFLAGS +=$(COPTIMIZE)
%.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
%.od: CFLAGS +=-O0 -g -D DEBUG
%.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
## Link options
-$(EXEC): LFLAGS += -g
+$(EXEC): LFLAGS +=
$(EXEC)_profile: LFLAGS += -g -pg
$(EXEC)_debug: LFLAGS += -g
#$(EXEC)_release: LFLAGS += ...
@@ -69,12 +69,12 @@ lib$(LIB)_release.a: $(filter-out */Main.or, $(RCOBJS)
## Build rule
%.o %.op %.od %.or: %.cc
@echo Compiling: $(subst $(MROOT)/,,$@)
- @$(CXX) $(CFLAGS) -c -o $@ $<
+ $(CXX) $(CFLAGS) -c -o $@ $<
## Linking rules (standard/profile/debug/release)
$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
@echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
- @$(CXX) $^ $(LFLAGS) -o $@
+ $(CXX) $^ $(LFLAGS) -o $@
## Library rules (standard/profile/debug/release)
lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
@@ -94,7 +94,7 @@ clean:
## Make dependencies
depend.mk: $(CSRCS) $(CHDRS)
@echo Making dependencies
- @$(CXX) $(CFLAGS) -I$(MROOT) \
+ $(CXX) $(CFLAGS) -I$(MROOT) \
$(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
@for dir in $(DEPDIR); do \
if [ -r $(MROOT)/$${dir}/depend.mk ]; then \

19
math/minisat/patches/patch-simp_Main_cc
View File

@ -1,19 +0,0 @@
$OpenBSD: patch-simp_Main_cc,v 1.1 2010/08/19 14:19:22 edd Exp $
OpenBSD has no RLIMIT_AS
--- simp/Main.cc.orig Thu Aug 19 14:34:45 2010
+++ simp/Main.cc Thu Aug 19 14:35:07 2010
@@ -116,10 +116,10 @@ int main(int argc, char** argv)
if (mem_lim != INT32_MAX){
rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
rlimit rl;
- getrlimit(RLIMIT_AS, &rl);
+ getrlimit(RLIMIT_DATA, &rl);
if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
rl.rlim_cur = new_mem_lim;
- if (setrlimit(RLIMIT_AS, &rl) == -1)
+ if (setrlimit(RLIMIT_DATA, &rl) == -1)
printf("WARNING! Could not set resource limit: Virtual memory.\n");
} }

23
math/minisat/patches/patch-utils_System_cc
View File

@ -1,23 +0,0 @@
$OpenBSD: patch-utils_System_cc,v 1.1 2010/08/19 14:19:22 edd Exp $
* memUsed is the same as FreeBSD
* namespace typo
--- utils/System.cc.orig Sat Jul 10 17:07:36 2010
+++ utils/System.cc Tue Jul 13 10:26:09 2010
@@ -72,13 +72,13 @@ double Minisat::memUsedPeak() {
double peak = memReadPeak() / 1024;
return peak == 0 ? memUsed() : peak; }
-#elif defined(__FreeBSD__)
+#elif defined(__FreeBSD__) || defined(__OpenBSD__)
double Minisat::memUsed(void) {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
return (double)ru.ru_maxrss / 1024; }
-double MiniSat::memUsedPeak(void) { return memUsed(); }
+double Minisat::memUsedPeak(void) { return memUsed(); }
#elif defined(__APPLE__)

6
math/minisat/pkg/DESCR
View File

@ -1,6 +1,6 @@
MiniSat is a minimalistic, open-source Boolean satisfiability problem
(SAT) solver, developed to help researchers and developers alike to get
started on SAT.
started on SAT.
Some key features of MiniSat:
* Easy to modify. MiniSat is small and well-documented, and possibly
@ -15,5 +15,5 @@ Some key features of MiniSat:
tool, such as a model checker or a more generic constraint solver.
The OpenBSD package of MiniSAT installs two binaries:
minisat = A core version of the solver.
minisats = An extended solver with simplification capabilities.
minisat_core = A core version of the solver.
minisat = An extended solver with simplification capabilities.

31
math/minisat/pkg/PLIST
View File

@ -1,5 +1,28 @@
@comment $OpenBSD: PLIST,v 1.3 2011/11/02 19:18:35 sthen Exp $
@comment $OpenBSD: PLIST,v 1.4 2017/08/20 16:39:44 jca Exp $
@bin bin/minisat
@bin bin/minisats
share/doc/minisat/
share/doc/minisat/MiniSat.pdf
@bin bin/minisat_core
include/minisat/
include/minisat/core/
include/minisat/core/Dimacs.h
include/minisat/core/Solver.h
include/minisat/core/SolverTypes.h
include/minisat/mtl/
include/minisat/mtl/Alg.h
include/minisat/mtl/Alloc.h
include/minisat/mtl/Heap.h
include/minisat/mtl/IntMap.h
include/minisat/mtl/IntTypes.h
include/minisat/mtl/Map.h
include/minisat/mtl/Queue.h
include/minisat/mtl/Rnd.h
include/minisat/mtl/Sort.h
include/minisat/mtl/Vec.h
include/minisat/mtl/XAlloc.h
include/minisat/simp/
include/minisat/simp/SimpSolver.h
include/minisat/utils/
include/minisat/utils/Options.h
include/minisat/utils/ParseUtils.h
include/minisat/utils/System.h
lib/libminisat.a
@lib lib/libminisat.so.${LIBminisat_VERSION}