# 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