[gappa/f13/master] Initial import (#622173)

David A. Wheeler dwheeler at fedoraproject.org
Sun Sep 26 01:52:04 UTC 2010


commit cb16876f2878440687f1badecf09e858df649d7d
Author: David A. Wheeler <dwheeler at dwheeler.com>
Date:   Sat Sep 25 21:52:04 2010 -0400

    Initial import (#622173)

 .gitignore |    2 +
 gappa.spec |   88 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 sources    |    2 +
 3 files changed, 92 insertions(+), 0 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e69de29..26a1b1f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1,2 @@
+gappa-0.13.0.tar.gz
+gappa.pdf
diff --git a/gappa.spec b/gappa.spec
new file mode 100644
index 0000000..c116141
--- /dev/null
+++ b/gappa.spec
@@ -0,0 +1,88 @@
+Name:		gappa
+Version:	0.13.0
+Release:	4%{?dist}
+Summary:	Prove programs with floating-point or fixed-point arithmetic
+
+Group:		Applications/Productivity
+License:	GPLv2 or CeCILL
+URL:		http://gappa.gforge.inria.fr/
+Source0:	https://gforge.inria.fr/frs/download.php/26856/gappa-%{version}.tar.gz
+Source1:	http://gappa.gforge.inria.fr/gappa.pdf
+BuildRoot:	%(mktemp -ud %{_tmppath}/%{name}-%{version}-%{release}-XXXXXX)
+
+BuildRequires:	gmp-devel, mpfr-devel, boost-devel, flex, bison
+
+%description
+Gappa is a tool intended to help verifying and formally prove
+properties on numerical programs and circuits handling floating-point
+or fixed-point arithmetic.  This tool manipulates logical formulas
+stating the enclosures of expressions in some intervals.  Through the
+use of rounding operators as part of the expressions, Gappa is specially
+designed to deal with formulas that could appear when certifying numerical
+codes. In particular, Gappa makes it simple to bound computational errors
+due to floating-point arithmetic.  The tool and its documentation were
+written by Guillaume Melquiond.
+
+%prep
+%setup -q
+cp -p %SOURCE1 .
+
+
+%build
+%configure
+# "make check" return exit status, emailed to Guillaume Melquiond 2010-09-10:
+sed -i 's/\( cat "$$logtmp"; \\\)/\1\n\texit 1; \\/' testsuite/Makefile
+make %{?_smp_mflags}
+iconv -f latin1 -t utf8 COPYING > COPYING.UTF8 && \
+touch -r COPYING COPYING.UTF8 && \
+mv COPYING.UTF8 COPYING
+# We won't 'make html-doc'; that requires dvi2bitmap, which is unpackaged.
+
+
+%check
+# Simple test to see if gappa is working at all:
+cd src
+echo "x * x in [0, 1b2 {4, 2^(2)}]" > ,test1.correct
+echo "{ x in [-2,2] -> x * x in ? }" | ./gappa >,test1 2>&1
+tail -1 ,test1 > ,test1.short
+cmp ,test1.short ,test1.correct
+
+# That simple test worked, so run full test suite:
+cd ..
+make check
+
+
+%install
+rm -rf %{buildroot}
+make install DESTDIR=%{buildroot}
+
+
+%clean
+rm -rf %{buildroot}
+
+
+%files
+%defattr(-,root,root,-)
+%{_bindir}/gappa
+%doc AUTHORS COPYING COPYING.GPL README TODO NEWS gappa.pdf
+
+
+%changelog
+* Tue Sep 21 2010 David A. Wheeler <dwheeler at dwheeler.com> - 0.13.0-4
+- Removed now-incorrect comment.
+
+* Sat Sep 11 2010 David A. Wheeler <dwheeler at dwheeler.com> - 0.13.0-3
+- Removed documentation source code from package
+- Greatly simplified spec file.
+
+* Fri Sep 10 2010 David A. Wheeler <dwheeler at dwheeler.com> - 0.13.0-2
+- Respond to comments 1-2 in https://bugzilla.redhat.com/show_bug.cgi?id=622173
+- Simplify (drop variable definitions in configure, drop INSTALL file)
+- Preserve the timestamp of file COPYING
+- More macro use
+- Modified to use bundled testsuite as well
+- PDF manual added
+
+* Sat Aug  7 2010 David A. Wheeler <dwheeler at dwheeler.com> - 0.13.0-1
+- Initial packaging
+
diff --git a/sources b/sources
index e69de29..8a12662 100644
--- a/sources
+++ b/sources
@@ -0,0 +1,2 @@
+27a09741f6b4da4c46c85952102af651  gappa-0.13.0.tar.gz
+15be2bc2e5fc88ff5addea92b85c44ea  gappa.pdf


More information about the scm-commits mailing list