]>
Commit | Line | Data |
---|---|---|
8f33d8d4 JR |
1 | # |
2 | # Conditional build: | |
3 | %bcond_with tests # run testsuite (non-deterministic fail in micromega tests on 64bit arch) | |
4 | # | |
521adcea | 5 | Summary: The Coq Proof Assistant |
374d5475 | 6 | Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu |
680764bb | 7 | Name: coq |
72eff188 | 8 | Version: 8.3pl1 |
8bee228d | 9 | Release: 0.1 |
680764bb JR |
10 | License: GPL |
11 | Group: Applications/Math | |
12 | Vendor: INRIA Rocquencourt | |
5f0acdc3 | 13 | Source0: http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz |
72eff188 | 14 | # Source0-md5: 1869d22b337f5da59ba3bbe1433f9a3b |
8bee228d JR |
15 | Source1: coqide.desktop |
16 | Source2: coqide.xpm | |
5f0acdc3 | 17 | Patch0: %{name}-lablgtk2.patch |
3432574d | 18 | URL: http://coq.inria.fr/ |
5f0acdc3 | 19 | BuildRequires: bash |
680764bb | 20 | BuildRequires: emacs |
8bee228d JR |
21 | BuildRequires: hevea |
22 | BuildRequires: netpbm-progs | |
861daf7b | 23 | BuildRequires: ocaml >= 3.09.0 |
5f0acdc3 | 24 | BuildRequires: camlp5 >= 5.01 |
72eff188 | 25 | BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 |
5f0acdc3 | 26 | BuildRequires: sed >= 4.0 |
308e7511 | 27 | BuildRequires: texlive-latex-ams |
8bee228d | 28 | BuildRequires: texlive-latex-comment |
b46eabb1 | 29 | BuildRequires: texlive-latex-moreverb |
8edb6738 | 30 | BuildRequires: texlive-psutils |
8bee228d | 31 | BuildRequires: texlive-format-pdflatex |
680764bb JR |
32 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
33 | ||
34 | %description | |
35 | Coq is a proof assistant which: | |
bcd66107 | 36 | - allows to handle calculus assertions, |
37 | - check mechanically proofs of these assertions, | |
38 | - helps to find formal proofs, | |
39 | - extracts a certified program from the constructive proof of its | |
40 | formal specification. | |
3432574d | 41 | |
3f4e388b JR |
42 | %description -l pl.UTF-8 |
43 | Coq to narzędzie pomagające w udowadnianiu, które: | |
44 | - pozwala uporać się z twierdzeniami dotyczącymi rachunku | |
45 | różniczkowego, | |
46 | - mechanicznie sprawdzać dowody tych twierdzeń, | |
47 | - pomagać w znalezieniu formalnych dowodów, | |
48 | - wyciągać program o dowiedzionej poprawności z konstruktywnego | |
bcd66107 | 49 | dowodu jego formalnej specyfikacji. |
680764bb | 50 | |
9019ffc7 JR |
51 | %package emacs |
52 | Summary: Emacs mode and syntax for Coq | |
53 | Summary(pl.UTF-8): Tryb i składnia Coq dla Emacsa | |
54 | Group: Development/Tools | |
55 | Requires: %{name} = %{version}-%{release} | |
56 | ||
57 | %description emacs | |
58 | Emacs mode and suyntax files for Coq. | |
59 | ||
60 | %description emacs -l pl.UTF-8 | |
61 | Pliki trybu i składni Coq dla Emacsa. | |
62 | ||
63 | %package latex | |
64 | Summary: Coq documentation style for latex | |
65 | Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa | |
66 | Group: Development/Tools | |
67 | Requires: %{name} = %{version}-%{release} | |
68 | ||
69 | %description latex | |
70 | Coq documentation style for latex. | |
71 | ||
72 | %description latex -l pl.UTF-8 | |
73 | Styl dokumentacji Coq dla latexa. | |
74 | ||
680764bb JR |
75 | %prep |
76 | %setup -q | |
5f0acdc3 JR |
77 | %patch0 -p1 |
78 | ||
79 | %{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check | |
680764bb JR |
80 | |
81 | %build | |
82 | ./configure \ | |
83 | -bindir %{_bindir} \ | |
84 | -libdir %{_libdir}/coq \ | |
85 | -mandir %{_mandir} \ | |
2dc46485 | 86 | -docdir %{_docdir}/%{name}-%{version} \ |
680764bb | 87 | -emacs emacs \ |
8f33d8d4 | 88 | -browser "xdg-open %s" \ |
680764bb JR |
89 | -emacslib %{_datadir}/emacs/site-lisp \ |
90 | -opt \ | |
1c74cbbc | 91 | --coqdocdir %{_datadir}/texmf/tex/latex/misc \ |
8bee228d | 92 | --coqide opt |
680764bb | 93 | |
9019ffc7 | 94 | %{__make} -j1 world |
8f33d8d4 | 95 | %{?with_tests:%{__make} -j1 check} # Use native coq to compile theories |
680764bb JR |
96 | |
97 | %install | |
98 | rm -rf $RPM_BUILD_ROOT | |
8bee228d | 99 | install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} |
3432574d JB |
100 | |
101 | %{__make} -e install \ | |
102 | COQINSTALLPREFIX=$RPM_BUILD_ROOT/ | |
680764bb JR |
103 | # To install only locally the binaries compiled with absolute paths |
104 | ||
8bee228d JR |
105 | install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} |
106 | install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} | |
107 | ||
680764bb JR |
108 | %clean |
109 | rm -rf $RPM_BUILD_ROOT | |
110 | ||
111 | %files | |
112 | %defattr(644,root,root,755) | |
861daf7b | 113 | %attr(755,root,root) %{_bindir}/coq_makefile |
9019ffc7 | 114 | %attr(755,root,root) %{_bindir}/coq-tex |
680764bb | 115 | %attr(755,root,root) %{_bindir}/coqc |
2dc46485 JR |
116 | %attr(755,root,root) %{_bindir}/coqchk |
117 | %attr(755,root,root) %{_bindir}/coqchk.opt | |
680764bb | 118 | %attr(755,root,root) %{_bindir}/coqdep |
1c74cbbc | 119 | %attr(755,root,root) %{_bindir}/coqdoc |
5f0acdc3 | 120 | %attr(755,root,root) %{_bindir}/coqide* |
861daf7b JR |
121 | %attr(755,root,root) %{_bindir}/coqmktop |
122 | %attr(755,root,root) %{_bindir}/coqtop | |
123 | %attr(755,root,root) %{_bindir}/coqtop.byte | |
124 | %attr(755,root,root) %{_bindir}/coqtop.opt | |
1c74cbbc | 125 | %attr(755,root,root) %{_bindir}/coqwc |
861daf7b | 126 | %attr(755,root,root) %{_bindir}/gallina |
3432574d | 127 | %dir %{_libdir}/coq |
1c74cbbc | 128 | %{_libdir}/coq/* |
9019ffc7 JR |
129 | %{_mandir}/man1/coq_makefile.1* |
130 | %{_mandir}/man1/coq-tex.1* | |
680764bb | 131 | %{_mandir}/man1/coqc.1* |
2dc46485 JR |
132 | %{_mandir}/man1/coqchk.1* |
133 | %{_mandir}/man1/coqdep.1* | |
134 | %{_mandir}/man1/coqdoc.1* | |
2dc46485 | 135 | %{_mandir}/man1/coqide.1* |
9019ffc7 | 136 | %{_mandir}/man1/coqmktop.1* |
680764bb JR |
137 | %{_mandir}/man1/coqtop.1* |
138 | %{_mandir}/man1/coqtop.byte.1* | |
139 | %{_mandir}/man1/coqtop.opt.1* | |
1c74cbbc | 140 | %{_mandir}/man1/coqwc.1* |
2dc46485 | 141 | %{_mandir}/man1/gallina.1* |
8bee228d JR |
142 | %{_desktopdir}/coqide.desktop |
143 | %{_pixmapsdir}/coqide.xpm | |
9019ffc7 JR |
144 | |
145 | %files emacs | |
146 | %defattr(644,root,root,755) | |
147 | %{_datadir}/emacs/site-lisp/coq.el | |
148 | %{_datadir}/emacs/site-lisp/coq-db.el | |
149 | %{_datadir}/emacs/site-lisp/coq-font-lock.el | |
150 | %{_datadir}/emacs/site-lisp/coq-inferior.el | |
151 | %{_datadir}/emacs/site-lisp/coq-syntax.el | |
152 | ||
153 | %files latex | |
154 | %defattr(644,root,root,755) | |
155 | %{_datadir}/texmf/tex/latex/misc/coqdoc.sty |