blob: 30a1e577ddd28eb1f79a167a3f9a3966ee80d493 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
Name: coq
Version: 8.0
Release: 2
Summary: The Coq Proof Assistant
Copyright: freely redistributable
Group: Applications/Math
Vendor: INRIA & LRI
URL: http://coq.inria.fr
Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
Icon: petit-coq.gif
BuildRoot: /var/tmp/coq
%description
Coq is a proof assistant which:
- allows to handle calculus assertions,
- check mechanically proofs of these assertions,
- helps to find formal proofs,
- extracts a certified program from the constructive proof
of its formal specification,
Requires: ocaml >= 3.06
%define debug_package %{nil}
%prep
%setup
%build
./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-emacslib %{_datadir}/emacs/site-lisp \
-coqdocdir %{_datadir}/texmf/tex/latex/misc \
-opt -reals all -coqide no
make coq
%clean
rm -rf %{buildroot}
make clean
%install
rm -rf %{buildroot}
make -e COQINSTALLPREFIX=%{buildroot} install-coq
%define __spec_install_post /usr/lib/rpm/brp-compress
%files
%defattr(-,root,root)
%{_bindir}/*
%{_libdir}/coq
%{_mandir}/man1/*
%{_datadir}/emacs/site-lisp/*
%{_datadir}/texmf/tex/latex/misc/*
|
