# 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.
%define debug_package %{nil}
%define flocqdir %{_libdir}/coq/user-contrib/Flocq
%define coqver 8.7

Name:           coq-flocq
Version:        3.2.0
Release:        %mkrel 1
Summary:        Formalization of floating point numbers for Coq

Group:          Sciences/Computer science
License:        LGPLv3+
URL:            http://flocq.gforge.inria.fr/
Source0:        https://gforge.inria.fr/frs/download.php/file/38103/flocq-%{version}.tar.gz

BuildRequires:  coq => %{coqver}
Requires:       coq => %{coqver}

%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.

%prep
%setup -q -n flocq-%{version}

%build
# We do NOT want to specify --libdir, and we don't need CFLAGS, etc.
./configure

./remake all doc

%install
sed -i "s,%{_libdir},%{buildroot}%{_libdir}," Remakefile
./remake install

# Also install the source files
cp -p src/*.v %{buildroot}%{flocqdir}
cp -p src/Calc/*.v %{buildroot}%{flocqdir}/Calc
cp -p src/Core/*.v %{buildroot}%{flocqdir}/Core
cp -p src/IEEE754/*.v %{buildroot}%{flocqdir}/IEEE754
cp -p src/Pff/*.v %{buildroot}%{flocqdir}/Pff
cp -p src/Prop/*.v %{buildroot}%{flocqdir}/Prop

%files
%doc AUTHORS COPYING NEWS.md README.md html
%dir %{flocqdir}
%{flocqdir}/*.v
%{flocqdir}/*.vo
%{flocqdir}/Calc/
%{flocqdir}/Core/
%{flocqdir}/IEEE754/
%{flocqdir}/Pff/
%{flocqdir}/Prop/



%changelog
* Mon Mar 02 2020 daviddavid <daviddavid> 3.2.0-1.mga8
+ Revision: 1552907
- new version: 3.2.0
+ umeabot <umeabot>
- Mageia 8 Mass Rebuild

* Sun Sep 30 2018 daviddavid <daviddavid> 2.6.0-3.mga7
+ Revision: 1312635
- rebuild against coq

* Sun Sep 23 2018 umeabot <umeabot> 2.6.0-2.mga7
+ Revision: 1296799
- Mageia 7 Mass Rebuild

* Mon Dec 04 2017 tv <tv> 2.6.0-1.mga7
+ Revision: 1181268
- new release

* Sun Sep 18 2016 daviddavid <daviddavid> 2.5.1-2.mga6
+ Revision: 1053655
- rebuild for new coq 8.5pl2
- fix some ownership flocq dir

* Tue Feb 02 2016 pterjan <pterjan> 2.5.1-1.mga6
+ Revision: 932970
- Update to 2.5.1
+ umeabot <umeabot>
- Mageia 6 Mass Rebuild

* Wed Oct 15 2014 umeabot <umeabot> 2.3.0-3.mga5
+ Revision: 740576
- Second Mageia 5 Mass Rebuild

* Tue Sep 16 2014 umeabot <umeabot> 2.3.0-2.mga5
+ Revision: 678544
- Mageia 5 Mass Rebuild

* Sun Jul 06 2014 pterjan <pterjan> 2.3.0-1.mga5
+ Revision: 644206
- 2.3.0

* Fri Nov 29 2013 malo <malo> 2.1.0-1.mga4
+ Revision: 554097
- fix RPM group
- spec clean-up after import from Fedora
- imported package coq-flocq


* Tue May 14 2013 Jerry James <loganjerry@gmail.com> - 2.1.0-5
- Rebuild for coq 8.4pl2

* Wed Feb 13 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.1.0-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild

* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 2.1.0-3
- Rebuild for coq 8.4pl1

* Tue Aug 21 2012 Jerry James <loganjerry@gmail.com> - 2.1.0-2
- Rebuild for coq 8.4

* Sat Jul 28 2012 Jerry James <loganjerry@gmail.com> - 2.1.0-1
- New upstream release
- Build for OCaml 4.0.0 and coq 8.3pl4

* Thu Jul 19 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.0.0-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild

* Sat Jan  7 2012 Jerry James <loganjerry@gmail.com> - 2.0.0-3
- Rebuild for OCaml 3.12.1

* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 2.0.0-2
- Rebuild for coq 8.3pl3

* Mon Dec 12 2011 Jerry James <loganjerry@gmail.com> - 2.0.0-1
- New upstream release
- Change subpackage from -devel to -source to match gappalib-coq.

* Fri Oct 28 2011 Jerry James <loganjerry@gmail.com> - 1.4.0-3
- Fix broken version numbers in BR and Requires

* Wed Oct 26 2011 Jerry James <loganjerry@gmail.com> - 1.4.0-2
- Split out a -devel subpackage

* Tue Jul  5 2011 Jerry James <loganjerry@gmail.com> - 1.4.0-1
- Initial RPM