]>
Commit | Line | Data |
---|---|---|
521adcea | 1 | Summary: The Coq Proof Assistant |
3f4e388b | 2 | Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu |
680764bb | 3 | Name: coq |
54bf5b31 | 4 | Version: 8.0pl2 |
861daf7b | 5 | Release: 2 |
680764bb JR |
6 | License: GPL |
7 | Group: Applications/Math | |
8 | Vendor: INRIA Rocquencourt | |
54bf5b31 | 9 | Source0: ftp://ftp.inria.fr/INRIA/coq/V%{version}/%{name}-%{version}.tar.gz |
10 | # Source0-md5: 39ee0fed76e47a11de2f49e2c236ef79 | |
861daf7b JR |
11 | # ftp://ftp.inria.fr/INRIA/coq/V8.0pl2/patch-coq-8.0pl2-ocaml-3.09 |
12 | Patch0: %{name}-ocaml-3.09.patch | |
13 | Patch1: %{name}-lablgtk26.patch | |
3432574d | 14 | URL: http://coq.inria.fr/ |
680764bb | 15 | BuildRequires: emacs |
861daf7b | 16 | BuildRequires: ocaml >= 3.09.0 |
54bf5b31 | 17 | BuildRequires: ocaml-camlp4 |
861daf7b | 18 | BuildRequires: ocaml-lablgtk2-devel >= 2.6.0 |
680764bb JR |
19 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
20 | ||
21 | %description | |
22 | Coq is a proof assistant which: | |
bcd66107 | 23 | - allows to handle calculus assertions, |
24 | - check mechanically proofs of these assertions, | |
25 | - helps to find formal proofs, | |
26 | - extracts a certified program from the constructive proof of its | |
27 | formal specification. | |
3432574d | 28 | |
3f4e388b JR |
29 | %description -l pl.UTF-8 |
30 | Coq to narzędzie pomagające w udowadnianiu, które: | |
31 | - pozwala uporać się z twierdzeniami dotyczącymi rachunku | |
32 | różniczkowego, | |
33 | - mechanicznie sprawdzać dowody tych twierdzeń, | |
34 | - pomagać w znalezieniu formalnych dowodów, | |
35 | - wyciągać program o dowiedzionej poprawności z konstruktywnego | |
bcd66107 | 36 | dowodu jego formalnej specyfikacji. |
680764bb JR |
37 | |
38 | %prep | |
39 | %setup -q | |
861daf7b JR |
40 | %patch0 -p0 |
41 | %patch1 -p1 | |
680764bb JR |
42 | |
43 | %build | |
44 | ./configure \ | |
45 | -bindir %{_bindir} \ | |
46 | -libdir %{_libdir}/coq \ | |
47 | -mandir %{_mandir} \ | |
48 | -emacs emacs \ | |
49 | -emacslib %{_datadir}/emacs/site-lisp \ | |
50 | -opt \ | |
1c74cbbc | 51 | --coqdocdir %{_datadir}/texmf/tex/latex/misc \ |
861daf7b | 52 | --coqide opt \ |
1c74cbbc | 53 | -reals all # Need ocamlc.opt and ocamlopt.opt |
680764bb | 54 | |
bcd66107 | 55 | %{__make} world check # Use native coq to compile theories |
680764bb JR |
56 | |
57 | %install | |
58 | rm -rf $RPM_BUILD_ROOT | |
3432574d JB |
59 | |
60 | %{__make} -e install \ | |
61 | COQINSTALLPREFIX=$RPM_BUILD_ROOT/ | |
680764bb JR |
62 | # To install only locally the binaries compiled with absolute paths |
63 | ||
64 | %clean | |
65 | rm -rf $RPM_BUILD_ROOT | |
66 | ||
67 | %files | |
68 | %defattr(644,root,root,755) | |
861daf7b JR |
69 | %attr(755,root,root) %{_bindir}/coq-interface |
70 | %attr(755,root,root) %{_bindir}/coq-interface.opt | |
71 | %attr(755,root,root) %{_bindir}/coq-tex | |
72 | %attr(755,root,root) %{_bindir}/coq_makefile | |
680764bb | 73 | %attr(755,root,root) %{_bindir}/coqc |
680764bb | 74 | %attr(755,root,root) %{_bindir}/coqdep |
1c74cbbc | 75 | %attr(755,root,root) %{_bindir}/coqdoc |
861daf7b JR |
76 | %attr(755,root,root) %{_bindir}/coqide.byte |
77 | %attr(755,root,root) %{_bindir}/coqide.opt | |
78 | %attr(755,root,root) %{_bindir}/coqmktop | |
79 | %attr(755,root,root) %{_bindir}/coqtop | |
80 | %attr(755,root,root) %{_bindir}/coqtop.byte | |
81 | %attr(755,root,root) %{_bindir}/coqtop.opt | |
1c74cbbc | 82 | %attr(755,root,root) %{_bindir}/coqwc |
861daf7b | 83 | %attr(755,root,root) %{_bindir}/gallina |
680764bb | 84 | %attr(755,root,root) %{_bindir}/parser |
1c74cbbc | 85 | %attr(755,root,root) %{_bindir}/parser.opt |
3432574d | 86 | %dir %{_libdir}/coq |
1c74cbbc | 87 | %{_libdir}/coq/* |
680764bb JR |
88 | %{_datadir}/emacs/site-lisp/coq.el |
89 | %{_datadir}/emacs/site-lisp/coq-inferior.el | |
90 | %{_mandir}/man1/coq-tex.1* | |
91 | %{_mandir}/man1/coqdep.1* | |
92 | %{_mandir}/man1/gallina.1* | |
93 | %{_mandir}/man1/coqc.1* | |
94 | %{_mandir}/man1/coqtop.1* | |
95 | %{_mandir}/man1/coqtop.byte.1* | |
96 | %{_mandir}/man1/coqtop.opt.1* | |
97 | %{_mandir}/man1/coq_makefile.1* | |
98 | %{_mandir}/man1/coqmktop.1* | |
99 | %{_mandir}/man1/coq-interface.1* | |
100 | %{_mandir}/man1/parser.1* | |
1c74cbbc | 101 | %{_mandir}/man1/coqdoc.1* |
102 | %{_mandir}/man1/coqwc.1* | |
103 | %{_datadir}/texmf/tex/latex/misc/coqdoc.sty |