sm-commit AT lists.ibiblio.org
Subject: Source Mage code commit list
List archive
[[SM-Commit] ] GIT changes to master grimoire by Ismael Luceno (2597f113537790f243b8d83da4d9f69d80aa7ea9)
- From: Ismael Luceno <scm AT sourcemage.org>
- To: sm-commit AT lists.ibiblio.org, sm-commit AT lists.sourcemage.org
- Subject: [[SM-Commit] ] GIT changes to master grimoire by Ismael Luceno (2597f113537790f243b8d83da4d9f69d80aa7ea9)
- Date: Thu, 15 May 2025 14:35:05 +0000
GIT changes to master grimoire by Ismael Luceno <ismael AT sourcemage.org>:
ChangeLog | 4
devel/cbmc/DEPENDS | 1
devel/cbmc/DETAILS | 4
devel/cbmc/HISTORY | 4
science-libs/minisat/BUILD | 2
science-libs/minisat/DETAILS | 29
++++++
science-libs/minisat/HISTORY | 3
science-libs/minisat/INSTALL | 1
science-libs/minisat/PRE_BUILD | 3
science-libs/minisat/patches/0001-Fix-build-against-musl-libc.patch | 42
++++++++++
10 files changed, 91 insertions(+), 2 deletions(-)
New commits:
commit 2597f113537790f243b8d83da4d9f69d80aa7ea9
Author: Ismael Luceno <ismael AT sourcemage.org>
Commit: Ismael Luceno <ismael AT sourcemage.org>
cbmc 6.6.0
commit 17522f7ebebcc47205bb191fa1017c6c865793c6
Author: Ismael Luceno <ismael AT sourcemage.org>
Commit: Ismael Luceno <ismael AT sourcemage.org>
minisat: new spell, minimalistic, open-source SAT solver
diff --git a/ChangeLog b/ChangeLog
index 606fb1a..314c0b5 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,7 @@
+2025-05-15 Ismael Luceno <ismael AT sourcemage.org>
+ * science-libs/minisat: new spell, minimalistic, open-source SAT
+ solver
+
2025-05-12 Treeve Jelbert <treeve AT sourcemage.org>
* libs/wcslib: added, 'Representations of world coordinates in FITS'
* libs/readstat: added, read statistics files
diff --git a/devel/cbmc/DEPENDS b/devel/cbmc/DEPENDS
index 8a5d482..71b6899 100755
--- a/devel/cbmc/DEPENDS
+++ b/devel/cbmc/DEPENDS
@@ -1,3 +1,4 @@
+depends minisat &&
optional_depends JAVA \
'-DWITH_JBMC=on' \
'-DWITH_JBMC=off' \
diff --git a/devel/cbmc/DETAILS b/devel/cbmc/DETAILS
index 2286ef7..19d47a0 100755
--- a/devel/cbmc/DETAILS
+++ b/devel/cbmc/DETAILS
@@ -1,9 +1,9 @@
# Watch: https://github.com/diffblue/cbmc/tags cbmc-([0-9.]+)[.]tar
SPELL=cbmc
- VERSION=6.4.1
+ VERSION=6.6.0
SOURCE="$SPELL-$VERSION.tar.gz"
SOURCE_URL[0]=https://github.com/diffblue/cbmc/archive/$SOURCE
-
SOURCE_HASH=sha512:74bfdae9c203e81f34584fbb5f4f3d8b3b25bb3b6ae1d9254ac6c0ccd28090d3a6a0b1d66899d71f3f3dac4fcebca1f046633d88d5b0ab09e53390402d7ed329
+
SOURCE_HASH=sha512:39859cd086ab6b5adfa81dda3b03cb21520f92ad56ed6fe2d66f8c6a25972739e72f8813361b116195ee3d521210a9270cf26c1a3a9bc7c3bd1e203399ce39c2
SOURCE_DIRECTORY="$BUILD_DIRECTORY/cbmc-cbmc-$VERSION"
WEB_SITE="http://www.cprover.org/cbmc"
LICENSE[0]=BSD-4
diff --git a/devel/cbmc/HISTORY b/devel/cbmc/HISTORY
index 8a8cffc..2c374ea 100644
--- a/devel/cbmc/HISTORY
+++ b/devel/cbmc/HISTORY
@@ -1,3 +1,7 @@
+2025-05-15 Ismael Luceno <ismael AT sourcemage.org>
+ * DETAILS: updated spell to 6.6.0
+ * DEPENDS: added minisat
+
2025-02-01 Ismael Luceno <ismael AT sourcemage.org>
* DETAILS: updated spell to 6.4.1
diff --git a/science-libs/minisat/BUILD b/science-libs/minisat/BUILD
new file mode 100755
index 0000000..534561c
--- /dev/null
+++ b/science-libs/minisat/BUILD
@@ -0,0 +1,2 @@
+CFLAGS+=' -fpermissive -Wno-literal-suffix' &&
+default_build_make -C simp r MROOT="$PWD"
diff --git a/science-libs/minisat/DETAILS b/science-libs/minisat/DETAILS
new file mode 100755
index 0000000..a1bf982
--- /dev/null
+++ b/science-libs/minisat/DETAILS
@@ -0,0 +1,29 @@
+# Watch: http://minisat.se/downloads/
+ SPELL=minisat
+ VERSION=2.2.0
+ SOURCE="$SPELL-$VERSION.tar.gz"
+ SOURCE_URL[0]=http://minisat.se/downloads/$SOURCE
+
SOURCE_HASH=sha512:cf79b05d43ebdc8fd8081899a1f853370de051cafe6e5b143eaff9827efc542b58062782a3ce2a3d1a03561a9ffd780c9cdc645bb50036eb61e80fa729136e64
+SOURCE_DIRECTORY="$BUILD_DIRECTORY/$SPELL"
+ WEB_SITE="http://minisat.se/"
+ LICENSE[0]="MIT"
+ ENTERED=20250515
+ KEYWORDS=""
+ SHORT="minimalistic, open-source SAT solver"
+cat << EOF
+MiniSat is a minimalistic, open-source SAT solver, developed to help
+researchers and developers alike to get started on SAT.
+
+Some key features of MiniSat:
+
+* Easy to modify. MiniSat is small and well-documented, and possibly also
+ well-designed, making it an ideal starting point for adapting SAT based
+ techniques to domain specific problems.
+* Highly efficient. Winning all the industrial categories of the SAT 2005
+ competition, MiniSat is a good starting point both for future research in
+ SAT, and for applications using SAT.
+* Designed for integration. MiniSat supports incremental SAT and has
+ mechanisms for adding non-clausal constraints. By virtue of being easy to
+ modify, it is a good choice for integrating as a backend to another tool,
+ such as a model checker or a more generic constraint solver.
+EOF
diff --git a/science-libs/minisat/HISTORY b/science-libs/minisat/HISTORY
new file mode 100644
index 0000000..e79f266
--- /dev/null
+++ b/science-libs/minisat/HISTORY
@@ -0,0 +1,3 @@
+2025-05-15 Ismael Luceno <ismael AT sourcemage.org>
+ * BUILD, DETAILS, INSTALL, PRE_BUILD,
+ patches/0001-Fix-build-against-musl-libc.patch: spell created
diff --git a/science-libs/minisat/INSTALL b/science-libs/minisat/INSTALL
new file mode 100755
index 0000000..5465ee0
--- /dev/null
+++ b/science-libs/minisat/INSTALL
@@ -0,0 +1 @@
+install -vD simp/minisat_release "$INSTALL_ROOT"/usr/bin/minisat
diff --git a/science-libs/minisat/PRE_BUILD b/science-libs/minisat/PRE_BUILD
new file mode 100755
index 0000000..c230ad1
--- /dev/null
+++ b/science-libs/minisat/PRE_BUILD
@@ -0,0 +1,3 @@
+default_pre_build &&
+cd "$SOURCE_DIRECTORY" &&
+apply_patch_dir patches
diff --git
a/science-libs/minisat/patches/0001-Fix-build-against-musl-libc.patch
b/science-libs/minisat/patches/0001-Fix-build-against-musl-libc.patch
new file mode 100644
index 0000000..6b2776e
--- /dev/null
+++ b/science-libs/minisat/patches/0001-Fix-build-against-musl-libc.patch
@@ -0,0 +1,42 @@
+From 80e2ee241403f82538a41a7b175947b6b438c630 Mon Sep 17 00:00:00 2001
+From: Ismael Luceno <ismael AT iodev.co.uk>
+Date: Thu, 15 May 2025 14:44:09 +0200
+Subject: [PATCH] Fix build against musl libc
+
+Origin: Source Mage
+Upstream-Status: Pending
+Signed-off-by: Ismael Luceno <ismael AT sourcemage.org>
+---
+ simp/Main.cc | 2 +-
+ utils/System.h | 2 +-
+ 2 files changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/utils/System.h b/utils/System.h
+index a51d4c2ee8d3..031014e96da4 100644
+--- a/utils/System.h
++++ b/utils/System.h
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
DEALINGS IN THE SOFTWA
+ #ifndef Minisat_System_h
+ #define Minisat_System_h
+
+-#if defined(__linux__)
++#if defined(__linux__) && defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
+diff --git a/simp/Main.cc b/simp/Main.cc
+index e59d73be0627..99ee47bea438 100644
+--- a/simp/Main.cc
++++ b/simp/Main.cc
+@@ -74,7 +74,7 @@ int main(int argc, char** argv)
+ setUsageHelp("USAGE: %s [options] <input-file>
<result-output-file>\n\n where input may be either in plain or gzipped
DIMACS.\n");
+ // printf("This is MiniSat 2.0 beta\n");
+
+-#if defined(__linux__)
++#if defined(__linux__) && defined(__GLIBC__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
_FPU_SETCW(newcw);
+ printf("WARNING: for repeatability, setting FPU to use double
precision\n");
+--
+2.49.0
+
- [[SM-Commit] ] GIT changes to master grimoire by Ismael Luceno (2597f113537790f243b8d83da4d9f69d80aa7ea9), Ismael Luceno, 05/15/2025
Archive powered by MHonArc 2.6.24.