# TESTING NOTE: The testsuite requires that gappalib-coq be installed already.
# Hence, we cannot run it on the koji builders. The maintainer should always
# install the package and run "make -C testsuite check" manually before
# committing.
%global gappadir %{_libdir}/coq/user-contrib/Gappa
%global coqver 8.4pl4
Name: gappalib-coq
Version: 1.0.0
Release: 8%{?dist}
Summary: Coq support library for gappa
Group: Applications/Engineering
License: LGPLv2+
URL: http://gappa.gforge.inria.fr/
Source0: https://gforge.inria.fr/frs/download.php/32743/%{name}-%{version}.tar.gz
BuildRequires: coq%{?_isa} = %{coqver}
BuildRequires: flocq
BuildRequires: gappa
BuildRequires: ocaml
BuildRequires: ocaml-camlp5-devel
BuildRequires: remake
Requires: coq%{?_isa} = %{coqver}
Requires: flocq
Requires: gappa
# This must match the corresponding line in the coq spec
ExclusiveArch: %{ocaml_arches}
%description
This support library provides vernacular files so that the certificates
Gappa generates can be imported by the Coq proof assistant. It also
provides a "gappa" tactic that calls Gappa on the current Coq goal.
Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques --
automatic proof generation of arithmetic properties) is a tool intended
to help verifying and formally proving properties on numerical programs
dealing with floating-point or fixed-point arithmetic.
%package source
Summary: Source Coq files
Requires: %{name}%{?_isa} = %{version}-%{release}
%description source
This package contains the source Coq files for gappalib-coq. These
files are not needed to use gappalib-coq. They are made available for
informational purposes.
%prep
%setup -q
# Enable debuginfo
sed -i 's/-pp/-g &/' Remakefile.in
%build
# The %%configure macro specifies --libdir, which this configure script
# unfortunately uses to identify where the Coq files should go. We want
# the default (i.e., ask coq itself where they go).
./configure --prefix=%{_prefix} --datadir=%{_datadir}
# Use the system remake
rm -f remake
ln -s %{_bindir}/remake remake
remake %{?_smp_mflags}
%install
sed -i '/^install:/,/^EXTRA_DIST/s, /usr, %{buildroot}%{_prefix},' Remakefile
mkdir -p %{buildroot}%{gappadir}
remake install
# Also install the source files
cp -p src/*.v %{buildroot}%{gappadir}
%files
%doc AUTHORS COPYING NEWS README
%{gappadir}
%exclude %{gappadir}/*.v
%files source
%{gappadir}/*.v
%changelog
* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-8
- Rebuild for coq 8.4pl4
* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-7
- Rebuild for flocq 2.3.0
* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-6
- Rebuild for flocq 2.2.2
* Wed Dec 18 2013 Jerry James <loganjerry@gmail.com> - 1.0.0-5
- Rebuild for coq 8.4pl3
* Mon Sep 16 2013 Jerry James <loganjerry@gmail.com> - 1.0.0-4
- Rebuild for OCaml 4.01.0
- Enable debuginfo
* Mon Aug 12 2013 Jerry James <loganjerry@gmail.com> - 1.0.0-3
- Rebuild for flocq 2.2.0
* Sat Aug 03 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.0.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
* Mon Jul 29 2013 Jerry James <loganjerry@gmail.com> - 1.0.0-1
- New upstream release
* Wed Jul 3 2013 Jerry James <loganjerry@gmail.com> - 0.21.1-1
- New upstream release
* Tue May 14 2013 Jerry James <loganjerry@gmail.com> - 0.20.0-1
- New upstream release
* Wed Feb 13 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.18.0-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
* Mon Jan 7 2013 Jerry James <loganjerry@gmail.com> - 0.18.0-6
- Rebuild for coq 8.4pl1
* Fri Oct 19 2012 Jerry James <loganjerry@gmail.com> - 0.18.0-5
- Rebuild for OCaml 4.00.1
* Tue Aug 21 2012 Jerry James <loganjerry@gmail.com> - 0.18.0-4
- Rebuild for coq 8.4
* Sat Jul 28 2012 Jerry James <loganjerry@gmail.com> - 0.18.0-3
- Rebuild for coq 8.3pl4, OCaml 4.00.0, and gappa 0.16.1
* Thu Jul 19 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.18.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
* Mon Jan 9 2012 Jerry James <loganjerry@gmail.com> - 0.18.0-1
- New upstream release
* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 0.17.0-2
- Rebuild for coq 8.3pl3
* Mon Dec 12 2011 Jerry James <loganjerry@gmail.com> - 0.17.0-1
- New upstream release
* Sat Oct 29 2011 Jerry James <loganjerry@gmail.com> - 0.16.0-3
- BR ocaml
* Wed Oct 26 2011 Jerry James <loganjerry@gmail.com> - 0.16.0-2
- Split out a -devel subpackage
* Tue Jul 5 2011 Jerry James <loganjerry@gmail.com> - 0.16.0-1
- Initial RPM