]>
Commit | Line | Data |
---|---|---|
8f33d8d4 | 1 | # |
857e15b1 JR |
2 | # TODO: |
3 | # - package and R: Csdp (https://projects.coin-or.org/Csdp) | |
4 | # | |
8f33d8d4 | 5 | # Conditional build: |
48226845 JR |
6 | %bcond_without ocaml_opt # skip building native optimized binaries (bytecode is always built) |
7 | %bcond_with tests # run testsuite (csdp dependant micromega tests fail badly on x86_64) | |
8f33d8d4 | 8 | # |
48226845 JR |
9 | %ifnarch %{ix86} %{x8664} arm aarch64 ppc sparc sparcv9 |
10 | %undefine with_ocaml_opt | |
11 | %endif | |
12 | ||
521adcea | 13 | Summary: The Coq Proof Assistant |
374d5475 | 14 | Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu |
680764bb | 15 | Name: coq |
83437006 JB |
16 | Version: 8.4pl6 |
17 | Release: 1 | |
18 | License: LGPL v2.1 | |
680764bb | 19 | Group: Applications/Math |
7f3d6db5 | 20 | Source0: http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz |
83437006 | 21 | # Source0-md5: 2334a98b64578cb81d2b4127e327b368 |
8bee228d JR |
22 | Source1: coqide.desktop |
23 | Source2: coqide.xpm | |
5f0acdc3 | 24 | Patch0: %{name}-lablgtk2.patch |
3432574d | 25 | URL: http://coq.inria.fr/ |
5f0acdc3 | 26 | BuildRequires: bash |
680764bb | 27 | BuildRequires: emacs |
8bee228d JR |
28 | BuildRequires: hevea |
29 | BuildRequires: netpbm-progs | |
861daf7b | 30 | BuildRequires: ocaml >= 3.09.0 |
5f0acdc3 | 31 | BuildRequires: camlp5 >= 5.01 |
72eff188 | 32 | BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 |
5f0acdc3 | 33 | BuildRequires: sed >= 4.0 |
9e2234f9 | 34 | BuildRequires: texlive-fonts-cmextra |
83437006 | 35 | BuildRequires: texlive-fonts-cmsuper |
9e2234f9 | 36 | BuildRequires: texlive-fonts-other |
83437006 | 37 | BuildRequires: texlive-format-pdflatex |
308e7511 | 38 | BuildRequires: texlive-latex-ams |
8bee228d | 39 | BuildRequires: texlive-latex-comment |
b46eabb1 | 40 | BuildRequires: texlive-latex-moreverb |
83437006 JB |
41 | BuildRequires: texlive-latex-ucs |
42 | BuildRequires: texlive-makeindex | |
8edb6738 | 43 | BuildRequires: texlive-psutils |
83437006 JB |
44 | # hyperref.sty (from latex) requires ifxexex.sty (from xetex) |
45 | BuildRequires: texlive-xetex | |
f4499714 | 46 | %requires_eq ocaml-runtime |
680764bb JR |
47 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
48 | ||
49 | %description | |
50 | Coq is a proof assistant which: | |
bcd66107 | 51 | - allows to handle calculus assertions, |
52 | - check mechanically proofs of these assertions, | |
53 | - helps to find formal proofs, | |
54 | - extracts a certified program from the constructive proof of its | |
55 | formal specification. | |
3432574d | 56 | |
3f4e388b JR |
57 | %description -l pl.UTF-8 |
58 | Coq to narzędzie pomagające w udowadnianiu, które: | |
59 | - pozwala uporać się z twierdzeniami dotyczącymi rachunku | |
60 | różniczkowego, | |
61 | - mechanicznie sprawdzać dowody tych twierdzeń, | |
62 | - pomagać w znalezieniu formalnych dowodów, | |
63 | - wyciągać program o dowiedzionej poprawności z konstruktywnego | |
bcd66107 | 64 | dowodu jego formalnej specyfikacji. |
680764bb | 65 | |
9019ffc7 JR |
66 | %package emacs |
67 | Summary: Emacs mode and syntax for Coq | |
68 | Summary(pl.UTF-8): Tryb i składnia Coq dla Emacsa | |
69 | Group: Development/Tools | |
70 | Requires: %{name} = %{version}-%{release} | |
71 | ||
72 | %description emacs | |
73 | Emacs mode and suyntax files for Coq. | |
74 | ||
75 | %description emacs -l pl.UTF-8 | |
76 | Pliki trybu i składni Coq dla Emacsa. | |
77 | ||
78 | %package latex | |
79 | Summary: Coq documentation style for latex | |
80 | Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa | |
81 | Group: Development/Tools | |
82 | Requires: %{name} = %{version}-%{release} | |
83 | ||
84 | %description latex | |
85 | Coq documentation style for latex. | |
86 | ||
87 | %description latex -l pl.UTF-8 | |
88 | Styl dokumentacji Coq dla latexa. | |
89 | ||
680764bb JR |
90 | %prep |
91 | %setup -q | |
5f0acdc3 JR |
92 | %patch0 -p1 |
93 | ||
94 | %{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check | |
857e15b1 | 95 | %{__sed} -i -e 's|\(MAKE_TSOPTS=.*\) -s \(.*\)|\1 \2|' Makefile.build |
680764bb JR |
96 | |
97 | %build | |
98 | ./configure \ | |
99 | -bindir %{_bindir} \ | |
100 | -libdir %{_libdir}/coq \ | |
101 | -mandir %{_mandir} \ | |
2dc46485 | 102 | -docdir %{_docdir}/%{name}-%{version} \ |
650aa0b6 JR |
103 | -configdir %{_sysconfdir}/%{name} \ |
104 | -datadir %{_datadir}/%{name} \ | |
680764bb | 105 | -emacs emacs \ |
8f33d8d4 | 106 | -browser "xdg-open %s" \ |
680764bb | 107 | -emacslib %{_datadir}/emacs/site-lisp \ |
48226845 | 108 | %{?with_ocaml_opt:-opt} \ |
1c74cbbc | 109 | --coqdocdir %{_datadir}/texmf/tex/latex/misc \ |
48226845 | 110 | --coqide %{?with_ocaml_opt:opt}%{!?with_ocaml_opt:byte} |
680764bb | 111 | |
48226845 JR |
112 | %{__make} -j1 world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun |
113 | %{?with_tests:%{__make} -j1 check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories | |
680764bb JR |
114 | |
115 | %install | |
116 | rm -rf $RPM_BUILD_ROOT | |
8bee228d | 117 | install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} |
3432574d JB |
118 | |
119 | %{__make} -e install \ | |
120 | COQINSTALLPREFIX=$RPM_BUILD_ROOT/ | |
680764bb JR |
121 | # To install only locally the binaries compiled with absolute paths |
122 | ||
8bee228d JR |
123 | install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} |
124 | install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} | |
125 | ||
c10c241b JR |
126 | # pdf is enough |
127 | %{__rm} -r $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}/ps | |
83437006 | 128 | cp -p CHANGES COMPATIBILITY COPYRIGHT CREDITS README $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} |
c10c241b | 129 | |
680764bb JR |
130 | %clean |
131 | rm -rf $RPM_BUILD_ROOT | |
132 | ||
133 | %files | |
134 | %defattr(644,root,root,755) | |
c10c241b | 135 | %doc %{_docdir}/%{name}-%{version} |
650aa0b6 JR |
136 | %dir %{_sysconfdir}/%{name} |
137 | %config(noreplace) %verify(not md5 mtime size) %{_sysconfdir}/%{name}/coqide-gtk2rc | |
861daf7b | 138 | %attr(755,root,root) %{_bindir}/coq_makefile |
9019ffc7 | 139 | %attr(755,root,root) %{_bindir}/coq-tex |
680764bb | 140 | %attr(755,root,root) %{_bindir}/coqc |
2dc46485 | 141 | %attr(755,root,root) %{_bindir}/coqchk |
9e2234f9 | 142 | %{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqchk.opt} |
680764bb | 143 | %attr(755,root,root) %{_bindir}/coqdep |
1c74cbbc | 144 | %attr(755,root,root) %{_bindir}/coqdoc |
5f0acdc3 | 145 | %attr(755,root,root) %{_bindir}/coqide* |
861daf7b JR |
146 | %attr(755,root,root) %{_bindir}/coqmktop |
147 | %attr(755,root,root) %{_bindir}/coqtop | |
148 | %attr(755,root,root) %{_bindir}/coqtop.byte | |
9e2234f9 | 149 | %{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqtop.opt} |
1c74cbbc | 150 | %attr(755,root,root) %{_bindir}/coqwc |
861daf7b | 151 | %attr(755,root,root) %{_bindir}/gallina |
3432574d | 152 | %dir %{_libdir}/coq |
1c74cbbc | 153 | %{_libdir}/coq/* |
9019ffc7 JR |
154 | %{_mandir}/man1/coq_makefile.1* |
155 | %{_mandir}/man1/coq-tex.1* | |
680764bb | 156 | %{_mandir}/man1/coqc.1* |
2dc46485 JR |
157 | %{_mandir}/man1/coqchk.1* |
158 | %{_mandir}/man1/coqdep.1* | |
159 | %{_mandir}/man1/coqdoc.1* | |
2dc46485 | 160 | %{_mandir}/man1/coqide.1* |
9019ffc7 | 161 | %{_mandir}/man1/coqmktop.1* |
680764bb JR |
162 | %{_mandir}/man1/coqtop.1* |
163 | %{_mandir}/man1/coqtop.byte.1* | |
9e2234f9 | 164 | %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*} |
1c74cbbc | 165 | %{_mandir}/man1/coqwc.1* |
2dc46485 | 166 | %{_mandir}/man1/gallina.1* |
8bee228d JR |
167 | %{_desktopdir}/coqide.desktop |
168 | %{_pixmapsdir}/coqide.xpm | |
650aa0b6 | 169 | %{_datadir}/%{name} |
9019ffc7 JR |
170 | |
171 | %files emacs | |
172 | %defattr(644,root,root,755) | |
173 | %{_datadir}/emacs/site-lisp/coq.el | |
174 | %{_datadir}/emacs/site-lisp/coq-db.el | |
175 | %{_datadir}/emacs/site-lisp/coq-font-lock.el | |
176 | %{_datadir}/emacs/site-lisp/coq-inferior.el | |
177 | %{_datadir}/emacs/site-lisp/coq-syntax.el | |
178 | ||
179 | %files latex | |
180 | %defattr(644,root,root,755) | |
181 | %{_datadir}/texmf/tex/latex/misc/coqdoc.sty |