%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 - 1.3.2-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild * Tue Jun 27 2017 Richard W.M. Jones - 1.3.2-6 - OCaml 4.04.2 rebuild. * Fri May 12 2017 Richard W.M. Jones - 1.3.2-5 - OCaml 4.04.1 rebuild. * Fri Mar 24 2017 Jerry James - 1.3.2-4 - Rebuild to fix coq consistency issue * Fri Feb 10 2017 Fedora Release Engineering - 1.3.2-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild * Thu Jan 12 2017 Jerry James - 1.3.2-2 - Rebuild for coq 8.6 * Mon Nov 28 2016 Jerry James - 1.3.2-1 - New upstream release * Mon Nov 07 2016 Richard W.M. Jones - 1.3.1-4 - Rebuild for OCaml 4.04.0. * Fri Oct 28 2016 Jerry James - 1.3.1-3 - Rebuild for coq 8.5pl3 * Mon Oct 03 2016 Dan Horák - 1.3.1-2 - disable debuginfo subpackage on interpreted builds * Thu Sep 29 2016 Jerry James - 1.3.1-1 - New upstream release * Fri Jul 22 2016 Jerry James - 1.3.0-1 - New upstream release * Wed Jul 13 2016 Jerry James - 1.2.1-3 - Rebuild for coq 8.5pl2 * Fri Apr 22 2016 Jerry James - 1.2.1-2 - Rebuild for coq 8.5pl1 * Fri Feb 12 2016 Jerry James - 1.2.1-1 - New upstream release - Use camlp4 in preference to camlp5 * Wed Feb 03 2016 Fedora Release Engineering - 1.2.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild * Wed Oct 14 2015 Jerry James - 1.2.0-1 - New upstream release * Thu Jul 30 2015 Richard W.M. Jones - 1.1.0-3 - OCaml 4.02.3 rebuild. * Wed Jun 24 2015 Richard W.M. Jones - 1.1.0-2 - ocaml-4.02.2 final rebuild. * Mon Jun 22 2015 Jerry James - 1.1.0-1 - New upstream release * Wed Jun 17 2015 Richard W.M. Jones - 1.0.0-21 - ocaml-4.02.2 rebuild. * Wed Jun 17 2015 Fedora Release Engineering - 1.0.0-20 - Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild * Sat Apr 11 2015 Jerry James - 1.0.0-19 - Rebuild for coq 8.4pl6 * Tue Feb 17 2015 Richard W.M. Jones - 1.0.0-18 - ocaml-4.02.1 rebuild. * Thu Nov 6 2014 Jerry James - 1.0.0-17 - Rebuild for ocaml-camlp5 6.12 * Thu Oct 30 2014 Jerry James - 1.0.0-16 - Rebuild for coq 8.4pl5 * Tue Sep 2 2014 Jerry James - 1.0.0-15 - Rebuild for flocq 2.4.0 * Sun Aug 31 2014 Richard W.M. Jones - 1.0.0-14 - ocaml-4.02.0 final rebuild. * Mon Aug 25 2014 Jerry James - 1.0.0-13 - ocaml-4.02.0+rc1 rebuild. * Sat Aug 16 2014 Fedora Release Engineering - 1.0.0-12 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild * Mon Aug 4 2014 Jerry James - 1.0.0-12 - Add workaround for ocamlopt beta version string - Fix license handling * Sat Aug 02 2014 Richard W.M. Jones - 1.0.0-11 - ocaml-4.02.0-0.8.git10e45753.fc22 rebuild. * Sat Jun 07 2014 Fedora Release Engineering - 1.0.0-10 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild * Tue May 13 2014 Jerry James - 1.0.0-9 - Rebuild for coq 8.4pl4 * Mon Apr 21 2014 Jerry James - 1.0.0-8 - Rebuild for flocq 2.3.0 * Tue Apr 15 2014 Richard W.M. Jones - 1.0.0-7 - Remove ocaml_arches macro (RHBZ#1087794). * Mon Mar 24 2014 Jerry James - 1.0.0-6 - Rebuild for flocq 2.2.2 * Wed Dec 18 2013 Jerry James - 1.0.0-5 - Rebuild for coq 8.4pl3 * Mon Sep 16 2013 Jerry James - 1.0.0-4 - Rebuild for OCaml 4.01.0 - Enable debuginfo * Mon Aug 12 2013 Jerry James - 1.0.0-3 - Rebuild for flocq 2.2.0 * Sat Aug 03 2013 Fedora Release Engineering - 1.0.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild * Mon Jul 29 2013 Jerry James - 1.0.0-1 - New upstream release * Wed Jul 3 2013 Jerry James - 0.21.1-1 - New upstream release * Tue May 14 2013 Jerry James - 0.20.0-1 - New upstream release * Wed Feb 13 2013 Fedora Release Engineering - 0.18.0-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild * Mon Jan 7 2013 Jerry James - 0.18.0-6 - Rebuild for coq 8.4pl1 * Fri Oct 19 2012 Jerry James - 0.18.0-5 - Rebuild for OCaml 4.00.1 * Tue Aug 21 2012 Jerry James - 0.18.0-4 - Rebuild for coq 8.4 * Sat Jul 28 2012 Jerry James - 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 - 0.18.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild * Mon Jan 9 2012 Jerry James - 0.18.0-1 - New upstream release * Tue Dec 27 2011 Jerry James - 0.17.0-2 - Rebuild for coq 8.3pl3 * Mon Dec 12 2011 Jerry James - 0.17.0-1 - New upstream release * Sat Oct 29 2011 Jerry James - 0.16.0-3 - BR ocaml * Wed Oct 26 2011 Jerry James - 0.16.0-2 - Split out a -devel subpackage * Tue Jul 5 2011 Jerry James - 0.16.0-1 - Initial RPM