[picosat] * Thu Jan 27 2011 Jerry James <loganjerry at gmail.com> - 936-1 - Update to version 936. - Drop picosat
Jerry James
jjames at fedoraproject.org
Thu Jan 27 18:53:45 UTC 2011
commit a8a3e7f486c1a1ec95ac0b2f7028c2263d1f4d83
Author: Jerry James <loganjerry at gmail.com>
Date: Thu Jan 27 11:52:06 2011 -0700
* Thu Jan 27 2011 Jerry James <loganjerry at gmail.com> - 936-1
- Update to version 936.
- Drop picosat-sharedlib.patch, incorporated upstream.
- Add picosat-trace.patch, to support separate tracing and nontracing libs.
.gitignore | 2 +-
picomus.1 | 55 +++++++++++++++++++++++
picosat-proof-access.patch | 74 +++++++++++++++++---------------
picosat-sharedlib.patch | 42 ------------------
picosat-trace.patch | 65 ++++++++++++++++++++++++++++
picosat.1 | 102 +++++++++++++++++++++++---------------------
picosat.spec | 77 ++++++++++++++++++++++-----------
picosat.trace.1 | 1 +
sources | 2 +-
9 files changed, 268 insertions(+), 152 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index cb5b9cc..95897e0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-picosat-913.tar.gz
+picosat-936.tar.gz
diff --git a/picomus.1 b/picomus.1
new file mode 100644
index 0000000..0e38fc8
--- /dev/null
+++ b/picomus.1
@@ -0,0 +1,55 @@
+.TH "PICOMUS" "1" "Version 936" "PicoSAT" "User Commands"
+.SH "NAME"
+picomus \- Minimal Unsatisfiable Core (MUS) generator
+.SH "SYNOPSIS"
+.B picomus
+[\fIOPTION\fR]... [\fIINPUT\fR [\fIOUTPUT\fR]]
+.SH "DESCRIPTION"
+.\" Add any additional description here
+.PP
+PicoMUS is a satisfiability (SAT) solver that generates a minimal unsatisfiable
+core, using the PicoSAT library.
+
+.SH "OPTIONS"
+.TP
+.BI \-h
+print this command line option summary and exit
+
+.TP
+.BI \-v
+enable verbose output
+
+.PP
+If no input filename is given, or the input filename is "-", then standard
+input is used. If the output filename is "-", then standard output is used.
+If no output filename is given, then the MUS is computed but not printed.
+
+.SH "CONFORMING TO"
+.PP
+This program uses DIMACS CNF format as input. The output conforms to the
+standard SAT solver format used at SAT competitions.
+
+.SH "EXIT STATUS"
+.PP
+The output is a number of lines.
+Most of these will begin with "c" (comment), and give detailed
+technical information.
+The output line beginning with "s" declares whether or not
+it is satisfiable.
+The line "s SATISFIABLE" is produced if it is satisfiable
+(exit status 10),
+and "s UNSATISFIABLE" is produced if it is not satisfiable
+(exit status 20).
+
+.SH "AUTHORS"
+picomus was written by Armin Biere <biere at jku.at>
+.PP
+This man page was written by Jerry James.
+It is released to the public domain; you may use it in any way you wish.
+
+.SH "SEE ALSO"
+.PP
+\fIpicosat\fP(1), \fIminisat2\fP(1).
+
+.\" This documentation was written by Jerry James in 2011, and
+.\" is released to the public domain. Anyone can use it, in any way.
diff --git a/picosat-proof-access.patch b/picosat-proof-access.patch
index 8271cde..1db28e5 100644
--- a/picosat-proof-access.patch
+++ b/picosat-proof-access.patch
@@ -1,7 +1,6 @@
-diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
---- picosat-913.ORIG/picosat.c 2009-07-13 07:04:44.000000000 -0600
-+++ picosat-913/picosat.c 2009-09-02 12:24:48.428654095 -0600
-@@ -6112,6 +6112,160 @@
+--- picosat.c.orig 2011-01-27 10:01:38.659957334 -0700
++++ picosat.c 2011-01-27 11:04:58.282436570 -0700
+@@ -6310,6 +6310,168 @@ write_trace (FILE * file, int fmt)
#endif
}
@@ -9,16 +8,18 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+ * method to access the zhains without printing to a file
+ */
+
++#ifdef TRACE
+static int* proof = NULL;
+static int cursor = 0;
+#define PROOF_BLOCK 10000
+static int current_size;
+static void add_int_to_proof(int i)
+{
-+ if(cursor >= current_size){
-+ current_size += PROOF_BLOCK;
-+ proof = realloc(proof, current_size);
-+ }
++ if (cursor >= current_size)
++ {
++ current_size += PROOF_BLOCK;
++ proof = realloc(proof, current_size);
++ }
+ proof[cursor] = i;
+ cursor++;
+}
@@ -28,6 +29,7 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+{
+ return EXPORTIDX (idx);
+}
++
+static void
+my_trace_lits (Cls * cls)
+{
@@ -44,6 +46,7 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+
+ add_int_to_proof(0);
+}
++
+static void
+my_trace_zhain (unsigned idx, Zhn * zhain)
+{
@@ -67,13 +70,15 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+
+ for (p = zhain->znt; (byte = *p); p++, i += 7)
+ {
++ int id;
++
+ delta |= (byte & 0x7f) << i;
+ if (byte & 0x80)
+ continue;
+
+ this = prev + delta;
+
-+ int id = my_write_idx (this);
++ id = my_write_idx (this);
+ add_int_to_proof(id);
+
+ prev = this;
@@ -82,8 +87,8 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+ }
+
+ add_int_to_proof(0);
-+
+}
++
+static void
+my_trace_clause (unsigned idx, Cls * cls)
+{
@@ -92,30 +97,28 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+ assert (!cls->learned);
+ assert (CLS2IDX (cls) == idx);
+
-+ int id = my_write_idx (idx);
-+ add_int_to_proof(id);
++ add_int_to_proof (my_write_idx (idx));
+
+ my_trace_lits (cls);
+
+ add_int_to_proof(0);
+
+}
++
+static int*
-+get_proof()
++get_proof ()
+{
-+#ifdef TRACE
-+ if (proof != NULL){
-+ free(proof);
-+ }
-+ proof = malloc(PROOF_BLOCK * (sizeof(int)));
-+ current_size = PROOF_BLOCK;
-+ cursor = 0;
-+
-+
+ Cls *cls, ** p;
+ Zhn *zhain;
+ unsigned i;
+
++ if (proof != NULL)
++ free(proof);
++
++ proof = malloc(PROOF_BLOCK * (sizeof(int)));
++ current_size = PROOF_BLOCK;
++ cursor = 0;
++
+ core ();
+
+ for (p = SOC; p != EOC; p = NXC (p))
@@ -129,7 +132,7 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+ }
+ else
+ {
-+ assert (lclauses <= p && p < eol);
++ assert (lclauses <= p && p < eol);
+ i = LIDX2IDX (p - lclauses);
+ }
+
@@ -142,30 +145,33 @@ diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
+ my_trace_zhain (i, zhain);
+ }
+ }
-+ else if (cls)
++ else if (cls && cls->core)
+ {
-+ if (cls->core)
-+ my_trace_clause (i, cls);
++ my_trace_clause (i, cls);
+ }
+ }
+ add_int_to_proof(EOP);
+ return proof;
-+#endif
++ return NULL;
+}
++#endif
++
+int *
-+picosat_get_proof(){
++picosat_get_proof ()
++{
++#ifdef TRACE
+ return get_proof();
++#else
++ return NULL;
++#endif
+}
-+////
-+
+
static void
write_core_wrapper (FILE * file, int fmt)
{
-diff -dur picosat-913.ORIG/picosat.h picosat-913/picosat.h
---- picosat-913.ORIG/picosat.h 2009-07-13 07:04:44.000000000 -0600
-+++ picosat-913/picosat.h 2009-09-02 12:24:27.959725988 -0600
-@@ -178,6 +178,12 @@
+--- picosat.h.orig 2010-08-04 06:20:44.000000000 -0600
++++ picosat.h 2011-01-27 10:55:19.079788986 -0700
+@@ -206,6 +206,12 @@ int picosat_inc_max_var (void);
*/
void picosat_adjust (int max_idx);
diff --git a/picosat-trace.patch b/picosat-trace.patch
new file mode 100644
index 0000000..54b4da9
--- /dev/null
+++ b/picosat-trace.patch
@@ -0,0 +1,65 @@
+--- makefile.in.orig 2010-08-04 06:20:44.000000000 -0600
++++ makefile.in 2011-01-27 10:16:18.353728096 -0700
+@@ -8,10 +8,10 @@
+ rm -f makefile config.h
+ rm -f gmon.out *~
+
+-picosat: libpicosat.a app.o main.o
++picosat: libpicosat.so app.o main.o
+ $(CC) $(CFLAGS) -o $@ main.o app.o -L. -lpicosat
+
+-picomus: libpicosat.a picomus.o
++picomus: libpicosat.so picomus.o
+ $(CC) $(CFLAGS) -o $@ picomus.o -L. -lpicosat
+
+ app.o: app.c picosat.h makefile
+@@ -24,10 +24,10 @@
+ $(CC) $(CFLAGS) -c $<
+
+ picosat.o: picosat.c picosat.h makefile
+- $(CC) $(CFLAGS) -c $<
++ $(CC) $(CFLAGS) -fPIC -c $<
+
+ version.o: version.c config.h makefile
+- $(CC) $(CFLAGS) -c $<
++ $(CC) $(CFLAGS) -fPIC -c $<
+
+ config.h: makefile VERSION mkconfig # and actually picosat.c
+ rm -f $@; ./mkconfig > $@
+@@ -38,6 +38,6 @@
+
+ SONAME=-Xlinker -soname -Xlinker libpicosat.so
+ libpicosat.so: picosat.o version.o
+- $(CC) $(CFLAGS) -shared -o $@ picosat.o version.o $(SONAME)
++ $(CC) $(CFLAGS) -fPIC -shared -o $@ picosat.o version.o $(SONAME)
+
+ .PHONY: all clean
+--- picosat.c.orig 2010-08-04 06:20:44.000000000 -0600
++++ picosat.c 2011-01-27 10:01:38.659957334 -0700
+@@ -6481,7 +6481,7 @@
+ (void) file;
+ (void) fmt;
+ (void) f;
+- ABORT ("compiled without trace support");
++ ABORT ("compiled without trace support; please use picosat.trace instead");
+ #endif
+ }
+
+@@ -6900,7 +6900,7 @@
+ leave ();
+ }
+ #else
+- ABORT ("compiled without trace support");
++ ABORT ("compiled without trace support; please use picosat.trace instead");
+ #endif
+
+ return res;
+@@ -6938,7 +6938,7 @@
+ leave ();
+ }
+ #else
+- ABORT ("compiled without trace support");
++ ABORT ("compiled without trace support; please use picosat.trace instead");
+ #endif
+
+ return res;
diff --git a/picosat.1 b/picosat.1
index bf01f87..028703b 100644
--- a/picosat.1
+++ b/picosat.1
@@ -1,12 +1,12 @@
-.TH "PICOSAT" "1" "Version 913" "PicoSAT" "User Commands"
+.TH "PICOSAT" "1" "Version 936" "PicoSAT" "User Commands"
.SH "NAME"
-picosat \- Satisfiability (SAT) solver for boolean variables
+picosat \- Satisfiability (SAT) solver with proof and core support
.SH "SYNOPSIS"
.B picosat
[\fIOPTION\fR]... [\fIFILE\fR]
.SH "DESCRIPTION"
.\" Add any additional description here
-.PP
+.PP
PicoSAT is a satisfiability (SAT) solver for boolean variables in
boolean expressions.
A SAT solver can determine if it is possible to find assignments to boolean
@@ -16,87 +16,91 @@ a set of assignments that make the expression true.
Many problems can be broken down into a large SAT problem
(perhaps with thousands of variables), so SAT solvers have a variety
of uses.
+.PP
+The \fBpicosat\fP binary is built with options that provide for the greatest
+speed. A second binary, \fBpicosat.trace\fP, is built with proof and core
+capabilities, which incur some overhead.
.SH "OPTIONS"
-.TP
+.TP
.BI \-h
print this command line option summary and exit
-.TP
+.TP
.BI \-\-version
print version and exit
-.TP
+.TP
.BI \-\-config
print build configuration and exit
-.TP
+.TP
.BI \-v
enable verbose output
-.TP
+.TP
.BI \-f
ignore invalid header
-.TP
+.TP
.BI \-n
do not print satisfying assignment
-.TP
+.TP
.BI \-p
print formula in DIMACS format and exit
-.TP
+.TP
.BI \-a " <lit>"
start with an assumption
-.TP
+.TP
.BI \-l " <limit>"
set decision limit (no limit per default)
-.TP
+.TP
.BI \-i " <0|1>"
force FALSE respectively TRUE as default phase
-.TP
+.TP
.BI \-s " <seed>"
set random number generator seed (default 0)
-.TP
+.TP
.BI \-o " <output>"
set output file (<stdout> per default)
-.TP
+.TP
.BI \-t " <trace>"
-generate compact proof trace file
+generate compact proof trace file (use picosat.trace; see above)
-.TP
+.TP
.BI \-T " <trace>"
-generate extended proof trace file
+generate extended proof trace file (use picosat.trace; see above)
-.TP
+.TP
.BI \-r " <trace>"
-generate reverse unit propagation proof file
+generate reverse unit propagation proof file (use picosat.trace; see above)
-.TP
+.TP
.BI \-c " <core>"
-generate clausal core file in DIMACS format
+generate clausal core file in DIMACS format (use picosat.trace; see above)
-.TP
+.TP
.BI \-V " <core>"
generate file listing core variables
-.TP
+.TP
.BI \-U " <core>"
generate file listing used variables
-.PP
+.PP
If no input filename is given, standard input is used.
.SH "CONFORMING TO"
-.PP
+.PP
This program uses DIMACS CNF format as input.
-.PP
+.PP
Like many SAT solvers, this program requires that its input be in
conjunctive normal form (CNF or cnf) in DIMACS CNF format.
CNF is built from these building blocks:
@@ -105,27 +109,27 @@ CNF is built from these building blocks:
.I R term :
A term is either a boolean variable (e.g., x4)
or a negated boolean variable (NOT x4, written here as \-x4).
-.TP
+.TP
*
.I R clause :
A clause is a set of one or more terms, connected with OR
(written here as |); boolean variables may not repeat inside a clause.
-.TP
+.TP
*
.I R expression :
An expression is a set of one or more clauses,
each connected by AND (written here as &).
-.PP
+.PP
Any boolean expression can be converted into CNF.
-.PP
+.PP
DIMACS CNF format is a simple text format for CNF.
Every line beginning "c" is a comment.
The first non\-comment line must be of the form:
-.PP
+.PP
p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES
-.PP
+.PP
Each of the non\-comment lines afterwards defines a clause.
Each of these lines is a space\-separated list of variables;
a positive value means that corresponding variable
@@ -134,7 +138,7 @@ a positive value means that corresponding variable
Each line must end in a space and the number 0.
.SH "EXIT STATUS"
-.PP
+.PP
The output is a number of lines.
Most of these will begin with "c" (comment), and give detailed
technical information.
@@ -144,55 +148,55 @@ The line "s SATISFIABLE" is produced if it is satisfiable
(exit status 10),
and "s UNSATISFIABLE" is produced if it is not satisfiable
(exit status 20).
-.PP
+.PP
If it is satisfiable,
the output line beginning with "v" declares a set of variable settings
that satisfy all formulas.
For example:
-.PP
+.PP
v 1 \-2 \-3 \-4 5 0
-.PP
+.PP
Shows that there is a solution with variable 1 true, variables 2, 3, and 4
false, and variable 5 true.
.SH "EXAMPLE"
-.PP
+.PP
An example of CNF is:
-.PP
+.PP
(x1 | \-x5 | x4) &
(\-x1 | x5 | x3 | x4) &
(\-x3 | x4).
-.PP
+.PP
The DIMACS CNF format for the above set of expressions could be:
-.PP
+.PP
c Here is a comment.
p cnf 5 3
1 \-5 4 0
\-1 5 3 4 0
\-3 \-4 0
-.PP
+.PP
The "p cnf" line above means that this is SAT problem in CNF format with
5 variables and 3 clauses. The first line after it is the first clause,
meaning x1 | \-x5 | x4.
-.PP
+.PP
CNFs with conflicting requirements are not satisfiable.
For example, the following DIMACS CNF formatted data is not satisfiable,
because it requires that variable 1 always be true and also always be false:
-.PP
+.PP
c This is not satisfiable.
p cnf 2 2
\-1 0
1 0
.SH "AUTHORS"
-.PP
+picosat was written by Armin Biere <biere at jku.at>
+.PP
This man page was written by David A. Wheeler.
It is released to the public domain; you may use it in any way you wish.
.SH "SEE ALSO"
-.PP
-minisat2(1).
+.PP
+\fIpicomus\fP(1), \fIminisat2\fP(1).
.\" This documentation was written by David A. Wheeler in 2010, and
.\" is released to the public domain. Anyone can use it, in any way.
-
diff --git a/picosat.spec b/picosat.spec
index 57da4e6..c6db4ac 100644
--- a/picosat.spec
+++ b/picosat.spec
@@ -1,6 +1,6 @@
Name: picosat
-Version: 913
-Release: 2%{?dist}
+Version: 936
+Release: 1%{?dist}
Summary: A SAT solver
Group: Applications/Engineering
@@ -9,18 +9,17 @@ URL: http://fmv.jku.at/picosat/
Source0: http://fmv.jku.at/picosat/%{name}-%{version}.tar.gz
# Thanks to David Wheeler for the man page.
Source1: picosat.1
-# This patch was sent upstream on 2 June 2009 and (mostly) incorporated into
-# the unreleased upstream version 917. It does the following:
-# - Links the binary against a shared library instead of a static library.
-# - Does not build the static library.
-# - Gives the resulting library an soname.
-Patch0: picosat-sharedlib.patch
-# This patch is needed by csisat. I asked upstream about it on 2 June 2009,
-# and they tell me that the next release of picosat will include this
-# functionality, although implemented differently. Until that release, and
-# the corresponding adapation of the csisat code, though, we need this patch.
+# Man page link for picosat.trace
+Source2: picosat.trace.1
+# Man page for picomus
+Source3: picomus.1
+# This patch has not been sent upstream. It is specific to Fedora's build of
+# two distinct binaries, one with trace support and one without.
+Patch0: picosat-trace.patch
+# This patch is needed by csisat. Picosat now provides a limited API for
+# extracting proofs in memory (i.e., not via a file), but csisat has not yet
+# been adapted to that API.
Patch1: picosat-proof-access.patch
-BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
# gzip required (see app.c); find-requires can't see into C code to find it
Requires: gzip, %{name}-libs = %{version}-%{release}
@@ -47,19 +46,35 @@ Summary: Development files for PicoSAT
Requires: %{name}-libs = %{version}-%{release}
%description devel
-Headers and other develpment files for PicoSAT.
+Headers and other development files for PicoSAT.
%prep
%setup -q
-%patch0 -p1
-%patch1 -p1
+%patch0
+%patch1
%build
# The configure script is NOT autoconf-generated and chooses its own CFLAGS,
# so we mimic its effects instead of using it.
+
+# Build the version with trace support
+sed -e "s/@CC@/gcc/" \
+ -e "s/@CFLAGS@/${RPM_OPT_FLAGS} -DTRACE -DNDEBUG/" \
+ -e "s/-Xlinker libpicosat.so/-Xlinker libpicosat.so.0/" \
+ -e "s/libpicosat/libpicosat-trace/g" \
+ -e "s/-lpicosat/-lpicosat-trace/g" \
+ -e "s/@TARGETS@/libpicosat-trace.so picosat picomus/" \
+ makefile.in > makefile
+make %{?_smp_mflags}
+mv picosat picosat.trace
+
+# Build the fast version.
+# Note that picomus needs trace support, so we don't rebuild it.
+rm -f *.o *.s config.h
sed -e "s/@CC@/gcc/" \
- -e "s/@CFLAGS@/${RPM_OPT_FLAGS} -DSTATS -DTRACE -DNDEBUG/" \
- -e "s/@TARGETS@/picosat libpicosat.so/" \
+ -e "s/@CFLAGS@/${RPM_OPT_FLAGS} -DNDEBUG/" \
+ -e "s/-Xlinker libpicosat.so/-Xlinker libpicosat.so.0/" \
+ -e "s/@TARGETS@/libpicosat.so picosat/" \
makefile.in > makefile
make %{?_smp_mflags}
@@ -70,19 +85,22 @@ rm -rf $RPM_BUILD_ROOT
mkdir -p $RPM_BUILD_ROOT%{_includedir}
cp -p picosat.h $RPM_BUILD_ROOT%{_includedir}
-# Install the library
+# Install the libraries
mkdir -p $RPM_BUILD_ROOT%{_libdir}
+cp -p libpicosat-trace.so $RPM_BUILD_ROOT%{_libdir}/libpicosat-trace.so.0.0.%{version}
+ln -s libpicosat-trace.so.0.0.%{version} $RPM_BUILD_ROOT%{_libdir}/libpicosat-trace.so.0
+ln -s libpicosat-trace.so.0 $RPM_BUILD_ROOT%{_libdir}/libpicosat-trace.so
cp -p libpicosat.so $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0.0.%{version}
ln -s libpicosat.so.0.0.%{version} $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0
ln -s libpicosat.so.0 $RPM_BUILD_ROOT%{_libdir}/libpicosat.so
-# Install the binary
+# Install the binaries
mkdir -p $RPM_BUILD_ROOT%{_bindir}
-cp -p picosat $RPM_BUILD_ROOT%{_bindir}
+cp -p picosat picosat.trace picomus $RPM_BUILD_ROOT%{_bindir}
-# Install the man page
+# Install the man pages
mkdir -p $RPM_BUILD_ROOT%{_mandir}/man1
-cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_mandir}/man1
+cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} $RPM_BUILD_ROOT%{_mandir}/man1
%post libs -p /sbin/ldconfig
@@ -96,20 +114,29 @@ rm -rf $RPM_BUILD_ROOT
# installed, but not vice versa.
%files
%defattr(-,root,root,-)
-%{_bindir}/picosat
-%{_mandir}/man1/picosat.1*
+%{_bindir}/picosat*
+%{_bindir}/picomus
+%{_mandir}/man1/picosat*
+%{_mandir}/man1/picomus*
%files libs
%defattr(-,root,root,-)
%doc LICENSE NEWS
+%{_libdir}/libpicosat-trace.so.*
%{_libdir}/libpicosat.so.*
%files devel
%defattr(-,root,root,-)
%{_includedir}/picosat.h
+%{_libdir}/libpicosat-trace.so
%{_libdir}/libpicosat.so
%changelog
+* Thu Jan 27 2011 Jerry James <loganjerry at gmail.com> - 936-1
+- Update to version 936.
+- Drop picosat-sharedlib.patch, incorporated upstream.
+- Add picosat-trace.patch, to support separate tracing and nontracing libs.
+
* Tue Jan 19 2010 Jerry James <loganjerry at gmail.com> - 913-2
- Spec file cleanups from review
- Man page courtesy of David Wheeler
diff --git a/picosat.trace.1 b/picosat.trace.1
new file mode 100644
index 0000000..4c8637d
--- /dev/null
+++ b/picosat.trace.1
@@ -0,0 +1 @@
+.so picosat.1
diff --git a/sources b/sources
index 4251664..9ae54d6 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-e658fa16cd71ff2cafae190a905a93c6 picosat-913.tar.gz
+0ad8404c134653d1e40f8fcd3a93a991 picosat-936.tar.gz
More information about the scm-commits
mailing list