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