%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%if ! %opt
%global debug_package %{nil}
%endif
# 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 "remake check" manually before committing.
%global gappadir %{_libdir}/coq/user-contrib/Gappa
%global coqver 8.6
Name: gappalib-coq
Version: 1.3.2
Release: 7%{?dist}
Summary: Coq support library for gappa
License: LGPLv2+
URL: http://gappa.gforge.inria.fr/
Source0: https://gforge.inria.fr/frs/download.php/file/36350/%{name}-%{version}.tar.gz
# Patch to work with camlp4
Patch0: %{name}-camlp4.patch
BuildRequires: coq = %{coqver}
BuildRequires: flocq
BuildRequires: gappa
BuildRequires: ocaml
BuildRequires: ocaml-camlp4-devel
BuildRequires: remake
Requires: coq%{?_isa} = %{coqver}
Requires: flocq
Requires: gappa
%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
%patch0
# Enable debuginfo
sed -i 's/-pp/-g &/' Remakefile.in
# Workaround broken ocamlopt version detection with beta ocaml versions
sed -i 's/^\(ocamlopt_version=`.*\)\(`\)/\1 | cut -d+ -f1\2/' configure
%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 NEWS README
%license COPYING
%{gappadir}
%exclude %{gappadir}/*.v
%files source
%{gappadir}/*.v
%changelog
* Wed Jul 26 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.2-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 1.3.2-6
- OCaml 4.04.2 rebuild.
* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 1.3.2-5
- OCaml 4.04.1 rebuild.
* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 1.3.2-4
- Rebuild to fix coq consistency issue
* Fri Feb 10 2017 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.2-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 1.3.2-2
- Rebuild for coq 8.6
* Mon Nov 28 2016 Jerry James <loganjerry@gmail.com> - 1.3.2-1
- New upstream release
* Mon Nov 07 2016 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-4
- Rebuild for OCaml 4.04.0.
* Fri Oct 28 2016 Jerry James <loganjerry@gmail.com> - 1.3.1-3
- Rebuild for coq 8.5pl3
* Mon Oct 03 2016 Dan Horák <dan[at]danny.cz> - 1.3.1-2
- disable debuginfo subpackage on interpreted builds
* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 1.3.1-1
- New upstream release
* Fri Jul 22 2016 Jerry James <loganjerry@gmail.com> - 1.3.0-1
- New upstream release
* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 1.2.1-3
- Rebuild for coq 8.5pl2
* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 1.2.1-2
- Rebuild for coq 8.5pl1
* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 1.2.1-1
- New upstream release
- Use camlp4 in preference to camlp5
* Wed Feb 03 2016 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 1.2.0-1
- New upstream release
* Thu Jul 30 2015 Richard W.M. Jones <rjones@redhat.com> - 1.1.0-3
- OCaml 4.02.3 rebuild.
* Wed Jun 24 2015 Richard W.M. Jones <rjones@redhat.com> - 1.1.0-2
- ocaml-4.02.2 final rebuild.
* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 1.1.0-1
- New upstream release
* Wed Jun 17 2015 Richard W.M. Jones <rjones@redhat.com> - 1.0.0-21
- ocaml-4.02.2 rebuild.
* Wed Jun 17 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.0.0-20
- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
* Sat Apr 11 2015 Jerry James <loganjerry@gmail.com> - 1.0.0-19
- Rebuild for coq 8.4pl6
* Tue Feb 17 2015 Richard W.M. Jones <rjones@redhat.com> - 1.0.0-18
- ocaml-4.02.1 rebuild.
* Thu Nov 6 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-17
- Rebuild for ocaml-camlp5 6.12
* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-16
- Rebuild for coq 8.4pl5
* Tue Sep 2 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-15
- Rebuild for flocq 2.4.0
* Sun Aug 31 2014 Richard W.M. Jones <rjones@redhat.com> - 1.0.0-14
- ocaml-4.02.0 final rebuild.
* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-13
- ocaml-4.02.0+rc1 rebuild.
* Sat Aug 16 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.0.0-12
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
* Mon Aug 4 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-12
- Add workaround for ocamlopt beta version string
- Fix license handling
* Sat Aug 02 2014 Richard W.M. Jones <rjones@redhat.com> - 1.0.0-11
- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild.
* Sat Jun 07 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.0.0-10
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-9
- Rebuild for coq 8.4pl4
* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 1.0.0-8
- Rebuild for flocq 2.3.0
* Tue Apr 15 2014 Richard W.M. Jones <rjones@redhat.com> - 1.0.0-7
- Remove ocaml_arches macro (RHBZ#1087794).
* 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