|
|
|
|
##
|
|
|
|
|
## coq.spec -- OpenPKG RPM Package Specification
|
|
|
|
|
## Copyright (c) 2000-2021 OpenPKG Project <http://openpkg.org/>
|
|
|
|
|
##
|
|
|
|
|
## 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
|
|
|
|
|
|
