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