[flocq] Initial checkin.
Jerry James
jjames at fedoraproject.org
Thu Oct 27 03:06:04 UTC 2011
commit 0365c597b35a91b3336b0ba5efbd90cd48dbdccf
Author: Jerry James <loganjerry at gmail.com>
Date: Wed Oct 26 21:05:53 2011 -0600
Initial checkin.
.gitignore | 1 +
flocq.spec | 75 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
sources | 1 +
3 files changed, 77 insertions(+), 0 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e69de29..8ee39fb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1 @@
+/flocq-1.4.0.tar.gz
diff --git a/flocq.spec b/flocq.spec
new file mode 100644
index 0000000..ef66a81
--- /dev/null
+++ b/flocq.spec
@@ -0,0 +1,75 @@
+# This package is really noarch, but it has to be installed in an arch-specific
+# location, so we build it as an arch-specific package.
+%global debug_package %{nil}
+%global flocqdir %{_libdir}/coq/user-contrib/Flocq
+
+Name: flocq
+Version: 1.4.0
+Release: 2%{?dist}
+Summary: Formalization of floating point numbers for Coq
+
+Group: Applications/Engineering
+License: LGPLv3+
+URL: http://flocq.gforge.inria.fr/
+Source0: https://gforge.inria.fr/frs/download.php/28389/%{name}-%{version}.tar.gz
+
+BuildRequires: coq
+Requires: coq = %(coqc -v | sed -nr "s/.* version ([[:alnum:]\.]+) .*/\1/p")
+
+%description
+Flocq (Floats for Coq) is a floating-point formalization for the Coq
+system. It provides a comprehensive library of theorems on a
+multi-radix multi-precision arithmetic. It also supports efficient
+numerical computations inside Coq.
+
+%package devel
+Summary: Source Coq files
+Requires: %{name}%{?_isa} = %{version}-%{release}
+
+%description devel
+This package contains the source Coq files for flocq. These files are
+not needed by consuming packages.
+
+%prep
+%setup -q
+
+%build
+# We do NOT want to specify --libdir, and we don't need CFLAGS, etc.
+./configure
+
+# %%{?_smp_mflags} sometimes succeeds, sometimes fails...
+make all html
+
+%install
+make install DESTDIR=$RPM_BUILD_ROOT
+
+# Also install the source files
+cp -p src/Appli/*.v $RPM_BUILD_ROOT%{flocqdir}/Appli
+cp -p src/Calc/*.v $RPM_BUILD_ROOT%{flocqdir}/Calc
+cp -p src/Core/*.v $RPM_BUILD_ROOT%{flocqdir}/Core
+cp -p src/Prop/*.v $RPM_BUILD_ROOT%{flocqdir}/Prop
+
+%files
+%doc AUTHORS COPYING NEWS README html
+%dir %{flocqdir}
+%dir %{flocqdir}/Appli
+%dir %{flocqdir}/Calc
+%dir %{flocqdir}/Core
+%dir %{flocqdir}/Prop
+%{flocqdir}/Appli/*.vo
+%{flocqdir}/Calc/*.vo
+%{flocqdir}/Core/*.vo
+%{flocqdir}/Prop/*.vo
+
+%files devel
+%{flocqdir}/Appli/*.v
+%{flocqdir}/Calc/*.v
+%{flocqdir}/Core/*.v
+%{flocqdir}/Prop/*.v
+
+%changelog
+* Wed Oct 26 2011 Jerry James <loganjerry at gmail.com> - 1.4.0-2
+- Split out a -devel subpackage
+
+* Tue Jul 5 2011 Jerry James <loganjerry at gmail.com> - 1.4.0-1
+- Initial RPM
diff --git a/sources b/sources
index e69de29..0ca87cb 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+ab05156cbbcbca41c31b6fb1549a6987 flocq-1.4.0.tar.gz
More information about the scm-commits
mailing list