[glueminisat] Initial import (#812681).
jcp
jcp at fedoraproject.org
Fri Apr 27 19:22:15 UTC 2012
commit 1850e69581058772c2fd4dda5390a80500c4461f
Author: John C. Peterson <jcp at eskimo.com>
Date: Fri Apr 27 12:21:11 2012 -0700
Initial import (#812681).
.gitignore | 1 +
glueminisat-FPU.patch | 24 ++++++
glueminisat-intro.html | 93 +++++++++++++++++++++++
glueminisat-printf.patch | 188 ++++++++++++++++++++++++++++++++++++++++++++++
glueminisat-test.in | 8 ++
glueminisat.spec | 118 +++++++++++++++++++++++++++++
sources | 1 +
7 files changed, 433 insertions(+), 0 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e69de29..f1debb8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1 @@
+/glueminisat-2.2.5.tar.gz
diff --git a/glueminisat-FPU.patch b/glueminisat-FPU.patch
new file mode 100644
index 0000000..1926761
--- /dev/null
+++ b/glueminisat-FPU.patch
@@ -0,0 +1,24 @@
+diff -uNr glueminisat-2.2.5.orig/core/Main.cc glueminisat-2.2.5/core/Main.cc
+--- glueminisat-2.2.5.orig/core/Main.cc 2011-03-02 00:24:12.000000000 -0800
++++ glueminisat-2.2.5/core/Main.cc 2012-04-24 09:55:10.845923073 -0700
+@@ -80,7 +80,7 @@
+ 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(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
+ 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");
+diff -uNr glueminisat-2.2.5.orig/simp/Main.cc glueminisat-2.2.5/simp/Main.cc
+--- glueminisat-2.2.5.orig/simp/Main.cc 2011-03-02 00:57:40.000000000 -0800
++++ glueminisat-2.2.5/simp/Main.cc 2012-04-24 09:53:34.629957638 -0700
+@@ -80,7 +80,7 @@
+ 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(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
+ 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");
diff --git a/glueminisat-intro.html b/glueminisat-intro.html
new file mode 100644
index 0000000..af65885
--- /dev/null
+++ b/glueminisat-intro.html
@@ -0,0 +1,93 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
+<title>An Introduction to GlueMiniSat</title>
+<meta name="description" content="A brief user guide for the GlueMiniSat boolean satisfiability problem (SAT) solver.">
+<meta name="keywords" content="GlueMiniSat, SAT, satisfiability, boolean satisfiability solver, propositional satisfiability solver, formal methods">
+<meta name="generator" content="vim">
+</head>
+<body lang="en">
+<h1 align="center">An Introduction to GlueMiniSat</h1>
+<h2>Boolean, Propositional SAT Solvers</h2>
+The development of
+<a href="http://en.wikipedia.org/wiki/Satisfiability">boolean, propositional satisfiability</a>
+(SAT) solvers has been an active and fluid area of research since
+the 1990's. Most of the contemporary SAT solvers that are efficient,
+and complete are still based on the now 50 year old
+<a href="http://en.wikipedia.org/wiki/DPLL_algorithm">Davis, Putnam, Logemann, Loveland (DPLL) algorithm</a>
+with some unique <a href="http://en.wikipedia.org/wiki/Constraint_learning">constraint learning</a>
+algorithm. Many of the new ideas in the area of conflict-driven clause
+learning (CDCL) solvers are implemented using the open source
+<a href="http://minisat.se/">MiniSat</a> solver as a starting point.
+There is an active
+<a href=" http://groups.google.com/group/minisat">MiniSat developers forum</a>
+on Google groups. Given the fluid nature of the research, detailed
+documentation is sometimes hard to come by. This document will hopefully
+be of some help to users that have just recently become acquainted with
+the community.
+<p>
+<h2>About GlueMiniSat</h2>
+<p>
+GlueMiniSat is a
+<a href="http://en.wikipedia.org/wiki/Satisfiability">boolean, propositional satisfiability</a>
+(SAT) problem solver developed by Hidetomo Nabeshima, Koji Iwanuma, and Katsumi
+Inoue of the University of Yamanashi, Japan. It is a derivative work of
+the open source <a href="http://minisat.se/MiniSat.html">MiniSat 2.2</a>
+solver, and implements a form of the literal blocks distance (LBD) evaluation
+criteria to predict the quality of clauses learned when conflicts are
+encountered in the search process.
+</p>
+<h2>Background Theory</h2>
+<p>
+The underlying concepts of literal blocks distance were first introduced
+in reference <a href="#REF01">[1]</a>. The authors' implementation of LBD,
+the Glucose 1.0 SAT solver, performed admirably by placing 2-nd at the
+<a href="http://www.cril.univ-artois.fr/SAT09/">International 2009 SAT
+competition</a> in the Applications (UNSAT) category. Further information
+can be found at the <a href="http://www.lri.fr/~simon/glucose">Glucose Home Page</a>.
+</p>
+<p>
+GlueMiniSat uses a slightly restricted concept of LBD, called strict
+LBD, and a dynamic restart strategy based on local averages of the
+decision levels and the LBDs of learned clauses. Experimental results
+show that GlueMiniSat also performs very well on SAT instances that
+are unsatisfiable. GlueMiniSat earned 1-st place at the
+<a href="http://www.cril.univ-artois.fr/SAT11/">International 2011
+SAT competition </a> in the Applications (UNSAT) category, solving 126
+of 142 problem instances. A more detailed discussion of the author's
+variation of LBD in GlueMiniSat can be found in reference
+<a href="#REF02">[2]</a>.
+</p>
+<h2>Using GlueMiniSat</h2>
+<p>
+Since GlueMiniSat is based on the open source MiniSat 2.2 SAT solver, it
+supports all of the command line options that are supported by MiniSat 2.2.
+David Wheeler has written a short User Guide for MiniSat (reference
+<a href="#REF03">[3])</a>) that is accordingly applicable to GlueMiniSat.
+The document also provides a simple introduction to the boolean satisfiability
+problem making it useful to readers looking for a SAT tutorial.
+<p>
+Note that GlueMiniSat can also run as a "clone" of the MiniSat 2.2 or
+Glucose 1.0 SAT solvers by specifying the command line options -minisat
+or -glucose, respectively. A brief overview of the command line options
+that provide more detailed control of GlueMiniSat's implementation of LBD
+can be obtained by executing glueminisat with the --help-verb option.
+</p>
+<h2>References, Resources</h2>
+<p>
+<ol>
+<li value="1" id="REF01">"Predicting learnt clauses quality in modern SAT
+solvers" by Gilles Audemard and Laurent Simon, Proceedings of IJCAI-2009,
+pages 399-404, 2009.
+<a href="http://ijcai.org/papers09/Papers/IJCAI09-074.pdf">[PDF]</a>
+<li value="2" id="REF02">"System description of GlueMiniSat 2.2.5" by
+Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue, Mar 2011. From the
+<a href="http://glueminisat.nabelab.org/">GlueMiniSat Home Page</a>.
+<a href="http://glueminisat.nabelab.org/home/download/glueminisat2.2.5.pdf?attredirects=0&d=1">[PDF]</a>
+<li value="3" id="REF03"><a href="http://www.dwheeler.com/essays/minisat-user-guide.html">User Guide for MiniSat</a>
+by <a href="http://www.dwheeler.com">David Wheeler</a>.
+</ol>
+</p>
+</body>
+</html>
diff --git a/glueminisat-printf.patch b/glueminisat-printf.patch
new file mode 100644
index 0000000..cc60917
--- /dev/null
+++ b/glueminisat-printf.patch
@@ -0,0 +1,188 @@
+diff -uNr glueminisat-2.2.5.orig/core/Main.cc glueminisat-2.2.5/core/Main.cc
+--- glueminisat-2.2.5.orig/core/Main.cc 2011-03-02 00:24:12.000000000 -0800
++++ glueminisat-2.2.5/core/Main.cc 2012-04-24 10:15:41.887958169 -0700
+@@ -146,21 +146,21 @@
+ printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
+
+ if (S.verbosity > 0){
+- printf("===============================[ Problem Statistics ]===============================\n");
+- printf("| |\n"); }
++ printf("=============================[ Problem Statistics ]=============================\n");
++ printf("| |\n"); }
+
+ parse_DIMACS(in, S);
+ gzclose(in);
+ FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+
+ if (S.verbosity > 0){
+- printf("| Number of variables: %12d |\n", S.nVars());
+- printf("| Number of clauses: %12d |\n", S.nClauses()); }
++ printf("| Number of variables: %12d |\n", S.nVars());
++ printf("| Number of clauses: %12d |\n", S.nClauses()); }
+
+ double parsed_time = cpuTime();
+ if (S.verbosity > 0){
+- printf("| Parse time: %12.2f s |\n", parsed_time - initial_time);
+- printf("| |\n"); }
++ printf("| Parse time: %12.4f s |\n", parsed_time - initial_time);
++ printf("| |\n"); }
+
+ // Change to signal-handlers that will only notify the solver and allow it to terminate
+ // voluntarily:
+@@ -170,7 +170,7 @@
+ if (!S.simplify()){
+ if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+ if (S.verbosity > 0){
+- printf("=============================================================================\n");
++ printf("================================================================================\n");
+ printf("Solved by unit propagation\n");
+ printStats(S);
+ printf("\n"); }
+@@ -214,7 +214,7 @@
+ return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
+ #endif
+ } catch (OutOfMemoryException&){
+- printf("=============================================================================\n");
++ printf("================================================================================\n");
+ printf("INDETERMINATE\n");
+ exit(0);
+ }
+diff -uNr glueminisat-2.2.5.orig/core/Solver.cc glueminisat-2.2.5/core/Solver.cc
+--- glueminisat-2.2.5.orig/core/Solver.cc 2011-02-27 22:04:33.000000000 -0800
++++ glueminisat-2.2.5/core/Solver.cc 2012-04-24 10:10:42.733250577 -0700
+@@ -101,7 +101,7 @@
+ printf("act=%f\n", c.activity());
+ }
+ void Solver::printLog() {
+- printf("| %9d | %7d %8d %8d | %8d %6.0f %6.1f %6.1f | %6.3f %% |\n",
++ printf("|%9d|%7d %8d %8d|%8d %7.0f %7.1f %7.1f| %7.4f%%|\n",
+ (int)conflicts,
+ (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
+ nLearnts(), (double)learnts_literals/nLearnts(), (double)tot_lbds/nLearnts(), wholeDLVs/conflicts, progressEstimate()*100);
+@@ -862,7 +862,7 @@
+
+ // added by nabesima
+ if (verbosity >= 1) {
+- printf("< ReduceDB %-3"PRIu64" (%4"PRIu64" restarts, %4.0f cnfs/res, %4.1f%% reduced, %4db %5dg %5dg3) >\n",
++ printf("< ReduceDB%-3"PRIu64" (%4"PRIu64"restarts, %4.0fcnfs/res, %4.1f%%reduced, %4db %5dg %5dg3) >\n",
+ reduce_dbs, starts, (double)conflicts / starts, (double)nLearnts() / org_learnts * 100.0,
+ num_bin, num_glue, num_glue3);
+ printLog();
+@@ -1226,10 +1226,10 @@
+ printf("===============================================================================\n");
+ */
+ // modified by nabesima
+- printf("===============================[ Search Statistics ]================================\n");
+- printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
+- printf("| | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | |\n");
+- printf("====================================================================================\n");
++ printf("=============================[ Search Statistics ]==============================\n");
++ printf("|Conflicts| ORIGINAL | LEARNT | Progress|\n");
++ printf("| | Vars Clauses Literals| Clauses Lit/Cl LBD/Cl DLV/Cl| |\n");
++ printf("================================================================================\n");
+ }
+
+ // Search:
+@@ -1246,7 +1246,7 @@
+ if (verbosity >= 1) {
+ //printf("===============================================================================\n");
+ printLog();
+- printf("====================================================================================\n");
++ printf("================================================================================\n");
+ }
+
+
+@@ -1386,7 +1386,7 @@
+
+ relocAll(to);
+ if (verbosity >= 2)
+- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
++ printf("| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ to.moveTo(ca);
+ }
+diff -uNr glueminisat-2.2.5.orig/simp/Main.cc glueminisat-2.2.5/simp/Main.cc
+--- glueminisat-2.2.5.orig/simp/Main.cc 2011-03-02 00:57:40.000000000 -0800
++++ glueminisat-2.2.5/simp/Main.cc 2012-04-24 10:16:16.276234939 -0700
+@@ -150,20 +150,20 @@
+ printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
+
+ if (S.verbosity > 0){
+- printf("===============================[ Problem Statistics ]===============================\n");
+- printf("| |\n"); }
++ printf("=============================[ Problem Statistics ]=============================\n");
++ printf("| |\n"); }
+
+ parse_DIMACS(in, S);
+ gzclose(in);
+ FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+
+ if (S.verbosity > 0){
+- printf("| Number of variables: %12d |\n", S.nVars());
+- printf("| Number of clauses: %12d |\n", S.nClauses()); }
++ printf("| Number of variables: %12d |\n", S.nVars());
++ printf("| Number of clauses: %12d |\n", S.nClauses()); }
+
+ double parsed_time = cpuTime();
+ if (S.verbosity > 0)
+- printf("| Parse time: %12.2f s |\n", parsed_time - initial_time);
++ printf("| Parse time: %12.4f s |\n", parsed_time - initial_time);
+
+ // Change to signal-handlers that will only notify the solver and allow it to terminate
+ // voluntarily:
+@@ -173,13 +173,13 @@
+ S.eliminate(true);
+ double simplified_time = cpuTime();
+ if (S.verbosity > 0){
+- printf("| Simplification time: %12.2f s |\n", simplified_time - parsed_time);
+- printf("| |\n"); }
++ printf("| Simplification time: %12.4f s |\n", simplified_time - parsed_time);
++ printf("| |\n"); }
+
+ if (!S.okay()){
+ if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+ if (S.verbosity > 0){
+- printf("====================================================================================\n");
++ printf("================================================================================\n");
+ printf("Solved by simplification\n");
+ printStats(S);
+ printf("\n"); }
+@@ -191,7 +191,7 @@
+
+ if (dimacs){
+ if (S.verbosity > 0)
+- printf("=================================[ Writing DIMACS ]=================================\n");
++ printf("===============================[ Writing DIMACS ]===============================\n");
+ S.toDimacs((const char*)dimacs);
+ if (S.verbosity > 0)
+ printStats(S);
+@@ -234,7 +234,7 @@
+ return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
+ #endif
+ } catch (OutOfMemoryException&){
+- printf("====================================================================================\n");
++ printf("================================================================================\n");
+ printf("INDETERMINATE\n");
+ exit(0);
+ }
+diff -uNr glueminisat-2.2.5.orig/simp/SimpSolver.cc glueminisat-2.2.5/simp/SimpSolver.cc
+--- glueminisat-2.2.5.orig/simp/SimpSolver.cc 2010-07-10 09:07:36.000000000 -0700
++++ glueminisat-2.2.5/simp/SimpSolver.cc 2012-04-24 09:57:12.291351846 -0700
+@@ -655,7 +655,7 @@
+ }
+
+ if (verbosity >= 1 && elimclauses.size() > 0)
+- printf("| Eliminated clauses: %10.2f Mb |\n",
++ printf("| Eliminated clauses: %10.2f Mb |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+
+ return ok;
+@@ -711,7 +711,7 @@
+ relocAll(to);
+ Solver::relocAll(to);
+ if (verbosity >= 2)
+- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
++ printf("| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ to.moveTo(ca);
+ }
diff --git a/glueminisat-test.in b/glueminisat-test.in
new file mode 100644
index 0000000..8dfed73
--- /dev/null
+++ b/glueminisat-test.in
@@ -0,0 +1,8 @@
+c
+c start with comments
+c
+c
+p cnf 5 3
+1 -5 4 0
+-1 5 3 4 0
+-3 -4 0
diff --git a/glueminisat.spec b/glueminisat.spec
new file mode 100644
index 0000000..cc050b0
--- /dev/null
+++ b/glueminisat.spec
@@ -0,0 +1,118 @@
+
+Name: glueminisat
+Version: 2.2.5
+Release: 3%{?dist}
+Summary: Boolean SAT solver that implements literal blocks distance (LBD)
+
+License: MIT
+Group: Applications/Engineering
+URL: http://glueminisat.nabelab.org/
+# Fetching the URL below with recent releases of Chromium and Firefox works
+# fine. However, fetching it with Wget currently fails for me (with the
+# message: "File name too long"). Including the -O option with the explicit
+# filename for the tar ball seems to work around that issue. The URL provided
+# by the GlueMiniSat download page has some additional HTTP GET parameters
+# appended to it; "?attredirects=0&d=1" (without the quotes). RPM doesn't
+# seem to like them, so they are omitted from the URL tag value here.
+Source0: https://sites.google.com/a/nabelab.org/glueminisat/home/download/%{name}-%{version}.tar.gz
+# Simple test case input (from the 2004 International SAT Competition)
+Source1: %{name}-test.in
+# Short HTML document that provides links to various online help resources
+Source2: %{name}-intro.html
+# Don't try to set the FPU to double precision unless target CPU supports it
+Patch0: %{name}-FPU.patch
+# Cosmetic patch to keep progress messages under 80 characters (avoids wrap)
+Patch1: %{name}-printf.patch
+# Copies of both patches above sent to Hidetomo Nabeshima on Mon Apr 23, 2012
+BuildRequires: zlib-devel
+
+%description
+GlueMiniSat is a boolean, propositional satisfiability (SAT) problem
+solver. It is a derivative work of the open source MiniSat 2.2 solver,
+and implements a form of the literal blocks distance (LBD) evaluation
+criteria to predict the quality of clauses learned when conflicts are
+encountered in the search process.
+
+The underlying concepts of literal blocks distance were first introduced
+in the paper "Predicting learnt clauses quality in modern SAT solvers"
+by Gilles Audemard and Laurent Simon, Proceedings of IJCAI-2009, pages
+399-404, 2009. The authors' implementation of LBD, the Glucose 1.0 SAT
+solver, performed admirably by placing 2-nd at the International 2009
+SAT competition in the Applications (UNSAT) category.
+
+GlueMiniSat uses a slightly restricted concept of LBD, called strict
+LBD, and a dynamic restart strategy based on local averages of the
+decision levels and the LBDs of learned clauses. Experimental results
+show that GlueMiniSat also performs very well on SAT instances that
+are unsatisfiable. GlueMiniSat earned 1-st place at the International
+2011 SAT competition in the Applications (UNSAT) category, solving 126
+of 142 problem instances.
+
+GlueMiniSat supports the same command line options as MiniSat 2.2 (see the
+documentation from the minisat2 package). It can also run as a "clone"
+of the MiniSat 2.2 or Glucose 1.0 SAT solvers by specifying the command
+line options -minisat or -glucose, respectively.
+
+%prep
+%setup -q
+%patch0 -p1 -b .orig
+%patch1 -p1 -b .orig
+cp -p %{SOURCE1} .
+cp -p %{SOURCE2} .
+# Show key execution steps, so we can see that the right flags are used.
+sed -i 's/@$(CXX)/$(CXX)/' mtl/template.mk
+
+
+%build
+# Build "simp", which adds simplification capabilities, instead of just "core"
+# The target "r" signifies that we are building the "released" version
+make %{?_smp_mflags} -C simp r \
+ MROOT=`pwd` \
+ COPTIMIZE="${RPM_OPT_FLAGS} -ffloat-store" \
+ LFLAGS="${RPM_OPT_FLAGS} -ffloat-store -lz"
+cp -p simp/%{name}_release %{name}
+
+%install
+mkdir -p ${RPM_BUILD_ROOT}%{_bindir}
+install -m 0755 %{name} ${RPM_BUILD_ROOT}%{_bindir}
+
+%check
+# The test file "glueminisat-test.in" is a brief quote from
+# http://www.satcompetition.org/2004/format-solvers2004.html
+# Exit value is 10 for satisfiable, 20 for unsatisfiable
+./glueminisat glueminisat-test.in glueminisat-test.out || true
+echo
+echo "RESULTS:"
+cat glueminisat-test.out
+result=`head -1 glueminisat-test.out`
+if [ "$result" = "SAT" ]; then
+ echo "SUCCESS - Correctly found that it was satisfiable"
+ true
+else
+ echo "Failed test."
+ false
+fi
+
+%files
+%doc LICENSE README README.minisat
+%doc %{name}-intro.html %{name}-test.in %{name}-test.out
+%attr(755,root,root) %{_bindir}/%{name}
+
+%changelog
+* Wed Apr 25 2012 John C. Peterson <jcp at eskimo.com> - 2.2.5-3
+- Wrote an HTML "intro" document with links to David Wheeler's MiniSat tutorial
+- Fixed minor typo error in the comments about the URL tag value
+- Added some additional information to the package description
+
+* Tue Apr 24 2012 John C. Peterson <jcp at eskimo.com> - 2.2.5-2
+- Replaced the usage of redundant global "myname" with standard macro "name"
+- Replaced the occurrences of glueminisat with "name" macro in source, patches
+- Sent the patches to upstream (Hidetomo Nabeshima, the primary author)
+- Addition to glueminisat-printf.patch (based on feedback from author)
+
+* Sat Apr 14 2012 John C. Peterson <jcp at eskimo.com> - 2.2.5-1
+- Note that GlueMiniSat is a derivative work of the MiniSat 2.2 SAT solver
+- Initial RPM spec file is based on the one from the Fedora minisat2 package
+- Cosmetic patch to keep progress messages under 80 characters (avoids wrap)
+- Adapted the FPU patch from the Fedora minisat2 package
+
diff --git a/sources b/sources
index e69de29..6e29a1e 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+1b96e19f7c0c5e0bec8c26c4eead9261 glueminisat-2.2.5.tar.gz
More information about the scm-commits
mailing list