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

# The arch-specific parts of this package are Ocaml, which does not lend itself
# to debuginfo generation.
%global debug_package %{nil}
%global gappadir %{_libdir}/coq/user-contrib/Gappa
%global coqver 8.3pl2

Name:           gappalib-coq
Version:        0.17.0
Release:        1%{?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/29908/%{name}-%{version}.tar.gz

BuildRequires:  coq%{?_isa} = %{coqver}
BuildRequires:  flocq
BuildRequires:  gappa
BuildRequires:  ocaml
BuildRequires:  ocaml-camlp5-devel

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

%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}
make %{?_smp_mflags}

%install
make install DESTDIR=$RPM_BUILD_ROOT

# Also install the source files
cp -p src/*.v  $RPM_BUILD_ROOT%{gappadir}

# Strip the tactic
strip $RPM_BUILD_ROOT%{gappadir}/gappatac.cmxs

%files
%doc AUTHORS COPYING NEWS README
%{gappadir}
%exclude %{gappadir}/*.v

%files source
%{gappadir}/*.v

%changelog
* 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