## ## coq.spec -- OpenPKG RPM Package Specification ## Copyright (c) 2000-2018 OpenPKG Project ## ## Permission to use, copy, modify, and distribute this software for ## any purpose with or without fee is hereby granted, provided that ## the above copyright notice and this permission notice appear in all ## copies. ## ## THIS SOFTWARE IS PROVIDED ``AS IS'' AND ANY EXPRESSED OR IMPLIED ## WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF ## MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. ## IN NO EVENT SHALL THE AUTHORS AND COPYRIGHT HOLDERS AND THEIR ## CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, ## SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT ## LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF ## USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ## ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, ## OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT ## OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF ## SUCH DAMAGE. ## # package information Name: coq Summary: Coq Poof Assistent URL: https://coq.inria.fr/ Vendor: INRIA Packager: OpenPKG Project Distribution: OpenPKG Community Class: EVAL Group: Algorithm License: LGPL Version: 8.6 Release: 20161215 # list of sources Source0: https://coq.inria.fr/distrib/V%{version}/files/coq-%{version}.tar.gz # build information BuildPreReq: OpenPKG, openpkg >= 20160101, make, ocaml, camlp5, ocaml-findlib PreReq: OpenPKG, openpkg >= 20160101 %description Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching. %track prog coq = { version = %{version} url = https://coq.inria.fr/download regex = coq-(__VER__)\.tar\.gz } %prep %setup -q %build CC="%{l_cc}" \ CFLAGS="%{l_cflags -O}" \ CPPFLAGS="%{l_cppflags}" \ LDFLAGS="%{l_ldflags}" \ ./configure \ -prefix %{l_prefix} \ -mandir %{l_prefix}/man \ -usecamlp5 %{l_make} %{l_mflags -O} %install %{l_make} %{l_mflags} install COQINSTALLPREFIX=$RPM_BUILD_ROOT rm -rf $RPM_BUILD_ROOT%{l_prefix}/share/emacs rm -rf $RPM_BUILD_ROOT%{l_prefix}/share/doc strip $RPM_BUILD_ROOT%{l_prefix}/bin/* >/dev/null 2>&1 || true %{l_rpmtool} files -v -ofiles -r$RPM_BUILD_ROOT %{l_files_std} %files -f files %clean