]>
Commit | Line | Data |
---|---|---|
521adcea | 1 | Summary: The Coq Proof Assistant |
374d5475 | 2 | Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu |
680764bb | 3 | Name: coq |
72eff188 | 4 | Version: 8.3pl1 |
8bee228d | 5 | Release: 0.1 |
680764bb JR |
6 | License: GPL |
7 | Group: Applications/Math | |
8 | Vendor: INRIA Rocquencourt | |
5f0acdc3 | 9 | Source0: http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz |
72eff188 | 10 | # Source0-md5: 1869d22b337f5da59ba3bbe1433f9a3b |
8bee228d JR |
11 | Source1: coqide.desktop |
12 | Source2: coqide.xpm | |
5f0acdc3 | 13 | Patch0: %{name}-lablgtk2.patch |
3432574d | 14 | URL: http://coq.inria.fr/ |
5f0acdc3 | 15 | BuildRequires: bash |
680764bb | 16 | BuildRequires: emacs |
8bee228d JR |
17 | BuildRequires: hevea |
18 | BuildRequires: netpbm-progs | |
861daf7b | 19 | BuildRequires: ocaml >= 3.09.0 |
5f0acdc3 | 20 | BuildRequires: camlp5 >= 5.01 |
72eff188 | 21 | BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 |
5f0acdc3 | 22 | BuildRequires: sed >= 4.0 |
308e7511 | 23 | BuildRequires: texlive-latex-ams |
8bee228d | 24 | BuildRequires: texlive-latex-comment |
b46eabb1 | 25 | BuildRequires: texlive-latex-moreverb |
8bee228d | 26 | BuildRequires: texlive-format-pdflatex |
680764bb JR |
27 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
28 | ||
29 | %description | |
30 | Coq is a proof assistant which: | |
bcd66107 | 31 | - allows to handle calculus assertions, |
32 | - check mechanically proofs of these assertions, | |
33 | - helps to find formal proofs, | |
34 | - extracts a certified program from the constructive proof of its | |
35 | formal specification. | |
3432574d | 36 | |
3f4e388b JR |
37 | %description -l pl.UTF-8 |
38 | Coq to narzędzie pomagające w udowadnianiu, które: | |
39 | - pozwala uporać się z twierdzeniami dotyczącymi rachunku | |
40 | różniczkowego, | |
41 | - mechanicznie sprawdzać dowody tych twierdzeń, | |
42 | - pomagać w znalezieniu formalnych dowodów, | |
43 | - wyciągać program o dowiedzionej poprawności z konstruktywnego | |
bcd66107 | 44 | dowodu jego formalnej specyfikacji. |
680764bb JR |
45 | |
46 | %prep | |
47 | %setup -q | |
5f0acdc3 JR |
48 | %patch0 -p1 |
49 | ||
50 | %{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check | |
680764bb JR |
51 | |
52 | %build | |
53 | ./configure \ | |
54 | -bindir %{_bindir} \ | |
55 | -libdir %{_libdir}/coq \ | |
56 | -mandir %{_mandir} \ | |
8bee228d | 57 | -docdir %{_datadir}/coq/doc \ |
680764bb | 58 | -emacs emacs \ |
8bee228d | 59 | -browser 'iceweasel -remote "OpenURL(%s,new-tab)" || iceweasel %s &' \ |
680764bb JR |
60 | -emacslib %{_datadir}/emacs/site-lisp \ |
61 | -opt \ | |
1c74cbbc | 62 | --coqdocdir %{_datadir}/texmf/tex/latex/misc \ |
8bee228d | 63 | --coqide opt |
680764bb | 64 | |
5f0acdc3 | 65 | %{__make} -j1 world check # Use native coq to compile theories |
680764bb JR |
66 | |
67 | %install | |
68 | rm -rf $RPM_BUILD_ROOT | |
8bee228d | 69 | install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} |
3432574d JB |
70 | |
71 | %{__make} -e install \ | |
72 | COQINSTALLPREFIX=$RPM_BUILD_ROOT/ | |
680764bb JR |
73 | # To install only locally the binaries compiled with absolute paths |
74 | ||
8bee228d JR |
75 | install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} |
76 | install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} | |
77 | ||
680764bb JR |
78 | %clean |
79 | rm -rf $RPM_BUILD_ROOT | |
80 | ||
81 | %files | |
82 | %defattr(644,root,root,755) | |
861daf7b JR |
83 | %attr(755,root,root) %{_bindir}/coq-interface |
84 | %attr(755,root,root) %{_bindir}/coq-interface.opt | |
85 | %attr(755,root,root) %{_bindir}/coq-tex | |
86 | %attr(755,root,root) %{_bindir}/coq_makefile | |
680764bb | 87 | %attr(755,root,root) %{_bindir}/coqc |
680764bb | 88 | %attr(755,root,root) %{_bindir}/coqdep |
1c74cbbc | 89 | %attr(755,root,root) %{_bindir}/coqdoc |
5f0acdc3 | 90 | %attr(755,root,root) %{_bindir}/coqide* |
861daf7b JR |
91 | %attr(755,root,root) %{_bindir}/coqmktop |
92 | %attr(755,root,root) %{_bindir}/coqtop | |
93 | %attr(755,root,root) %{_bindir}/coqtop.byte | |
94 | %attr(755,root,root) %{_bindir}/coqtop.opt | |
1c74cbbc | 95 | %attr(755,root,root) %{_bindir}/coqwc |
861daf7b | 96 | %attr(755,root,root) %{_bindir}/gallina |
680764bb | 97 | %attr(755,root,root) %{_bindir}/parser |
1c74cbbc | 98 | %attr(755,root,root) %{_bindir}/parser.opt |
3432574d | 99 | %dir %{_libdir}/coq |
1c74cbbc | 100 | %{_libdir}/coq/* |
680764bb JR |
101 | %{_datadir}/emacs/site-lisp/coq.el |
102 | %{_datadir}/emacs/site-lisp/coq-inferior.el | |
103 | %{_mandir}/man1/coq-tex.1* | |
104 | %{_mandir}/man1/coqdep.1* | |
105 | %{_mandir}/man1/gallina.1* | |
106 | %{_mandir}/man1/coqc.1* | |
107 | %{_mandir}/man1/coqtop.1* | |
108 | %{_mandir}/man1/coqtop.byte.1* | |
109 | %{_mandir}/man1/coqtop.opt.1* | |
110 | %{_mandir}/man1/coq_makefile.1* | |
111 | %{_mandir}/man1/coqmktop.1* | |
112 | %{_mandir}/man1/coq-interface.1* | |
113 | %{_mandir}/man1/parser.1* | |
1c74cbbc | 114 | %{_mandir}/man1/coqdoc.1* |
115 | %{_mandir}/man1/coqwc.1* | |
116 | %{_datadir}/texmf/tex/latex/misc/coqdoc.sty | |
8bee228d JR |
117 | %{_desktopdir}/coqide.desktop |
118 | %{_pixmapsdir}/coqide.xpm |