]>
Commit | Line | Data |
---|---|---|
8f33d8d4 JR |
1 | # |
2 | # Conditional build: | |
10fd38a7 JB |
3 | %bcond_without ocaml_opt # native optimized binaries (bytecode is always built) |
4 | %bcond_with sse2 # SSE2 instructions | |
5 | %bcond_with doc # documentation | |
48226845 | 6 | %bcond_with tests # run testsuite (csdp dependant micromega tests fail badly on x86_64) |
8f33d8d4 | 7 | # |
10fd38a7 JB |
8 | %ifarch pentium4 %{x8664} x32 |
9 | %define with_sse2 1 | |
10 | %endif | |
11 | ||
39bb0263 | 12 | %ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 |
48226845 JR |
13 | %undefine with_ocaml_opt |
14 | %endif | |
15 | ||
521adcea | 16 | Summary: The Coq Proof Assistant |
374d5475 | 17 | Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu |
680764bb | 18 | Name: coq |
b2cb8983 | 19 | Version: 8.13.1 |
0d680645 | 20 | Release: 5 |
83437006 | 21 | License: LGPL v2.1 |
680764bb | 22 | Group: Applications/Math |
b2cb8983 JR |
23 | Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz |
24 | # Source0-md5: 03ebbf1034c224a0a3327db2d5688c29 | |
8bee228d JR |
25 | Source1: coqide.desktop |
26 | Source2: coqide.xpm | |
10fd38a7 | 27 | URL: https://coq.inria.fr/ |
5f0acdc3 | 28 | BuildRequires: bash |
b2cb8983 | 29 | BuildRequires: ocaml >= 1:4.05 |
5f0acdc3 | 30 | BuildRequires: camlp5 >= 5.01 |
b2cb8983 JR |
31 | BuildRequires: ocaml-dune > 2.5.0 |
32 | BuildRequires: ocaml-findlib >= 1.8.1 | |
33 | BuildRequires: ocaml-zarith-devel >= 1.10 | |
10fd38a7 JB |
34 | BuildRequires: ocaml-lablgtk3-devel >= 3.1.0 |
35 | BuildRequires: ocaml-lablgtk3-gtksourceview-devel >= 3.1.0 | |
5f0acdc3 | 36 | BuildRequires: sed >= 4.0 |
10fd38a7 JB |
37 | %if %{with doc} |
38 | BuildRequires: python3 >= 1:3 | |
39 | # TODO (and adjust package name) | |
40 | BuildRequires: python3-antlr4-python3-runtime >= 4.7.1 | |
41 | BuildRequires: python3-bs4 >= 4.0.6 | |
42 | BuildRequires: python3-pexpect >= 4.2.1 | |
43 | BuildRequires: python3-sphinx_rtd_theme >= 0.4.3 | |
44 | # TODO (and adjust package name) | |
45 | BuildRequires: python3-sphinxcontrib-bibtex >= 0.4.2 | |
46 | BuildRequires: sphinx-pdg >= 2.3.1 | |
47 | # TODO: update texlive packages list (or drop pdf building leaving only html) | |
9e2234f9 | 48 | BuildRequires: texlive-fonts-cmextra |
83437006 | 49 | BuildRequires: texlive-fonts-cmsuper |
9e2234f9 | 50 | BuildRequires: texlive-fonts-other |
83437006 | 51 | BuildRequires: texlive-format-pdflatex |
308e7511 | 52 | BuildRequires: texlive-latex-ams |
8bee228d | 53 | BuildRequires: texlive-latex-comment |
b46eabb1 | 54 | BuildRequires: texlive-latex-moreverb |
83437006 JB |
55 | BuildRequires: texlive-latex-ucs |
56 | BuildRequires: texlive-makeindex | |
8edb6738 | 57 | BuildRequires: texlive-psutils |
83437006 JB |
58 | # hyperref.sty (from latex) requires ifxexex.sty (from xetex) |
59 | BuildRequires: texlive-xetex | |
10fd38a7 JB |
60 | %endif |
61 | %if %{with sse2} | |
62 | Requires: cpuinfo(sse2) | |
63 | %endif | |
f4499714 | 64 | %requires_eq ocaml-runtime |
b2cb8983 | 65 | Obsoletes: coq-emacs < 8.13.1 |
3e0583a4 | 66 | # same as ocaml-zarith |
39bb0263 | 67 | ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 |
680764bb JR |
68 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
69 | ||
3809f5df JR |
70 | # Exclude private ocaml interfaces |
71 | %define _noautoreq ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\) | |
72 | ||
680764bb JR |
73 | %description |
74 | Coq is a proof assistant which: | |
bcd66107 | 75 | - allows to handle calculus assertions, |
76 | - check mechanically proofs of these assertions, | |
77 | - helps to find formal proofs, | |
78 | - extracts a certified program from the constructive proof of its | |
79 | formal specification. | |
3432574d | 80 | |
3f4e388b JR |
81 | %description -l pl.UTF-8 |
82 | Coq to narzędzie pomagające w udowadnianiu, które: | |
83 | - pozwala uporać się z twierdzeniami dotyczącymi rachunku | |
84 | różniczkowego, | |
85 | - mechanicznie sprawdzać dowody tych twierdzeń, | |
86 | - pomagać w znalezieniu formalnych dowodów, | |
b2cb8983 JR |
87 | - wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu |
88 | jego formalnej specyfikacji. | |
9019ffc7 JR |
89 | |
90 | %package latex | |
10fd38a7 JB |
91 | Summary: Coq documentation style for LaTeX |
92 | Summary(pl.UTF-8): Styl dokumentacji Coq dla LaTeXa | |
9019ffc7 JR |
93 | Group: Development/Tools |
94 | Requires: %{name} = %{version}-%{release} | |
95 | ||
96 | %description latex | |
10fd38a7 | 97 | Coq documentation style for LaTeX. |
9019ffc7 JR |
98 | |
99 | %description latex -l pl.UTF-8 | |
10fd38a7 | 100 | Styl dokumentacji Coq dla LaTeXa. |
9019ffc7 | 101 | |
680764bb JR |
102 | %prep |
103 | %setup -q | |
5f0acdc3 | 104 | |
b2cb8983 JR |
105 | %{__sed} -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install |
106 | %{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' configure.ml | |
10fd38a7 JB |
107 | %if %{with sse2} |
108 | %{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' configure.ml | |
109 | %endif | |
b2cb8983 JR |
110 | %{__sed} -i "s|-oc|-ccopt '%{rpmldflags}' -g &|" Makefile.build |
111 | %{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in Makefile.build | |
112 | ||
113 | %{__sed} -E -i -e '1s,#!\s*/usr/bin/env\s+python3(\s|$),#!%{__python3}\1,' \ | |
114 | tools/make-both-single-timing-files.py \ | |
115 | tools/make-both-time-files.py \ | |
116 | tools/make-one-time-file.py | |
117 | ||
118 | %{__sed} -E -i -e '1s,#!\s*/usr/bin/env\s+python2(\s|$),#!%{__python3}\1,' \ | |
119 | doc/tools/coqrst/notations/fontsupport.py | |
680764bb JR |
120 | |
121 | %build | |
122 | ./configure \ | |
123 | -bindir %{_bindir} \ | |
650aa0b6 | 124 | -configdir %{_sysconfdir}/%{name} \ |
6b871b2b | 125 | -coqdocdir %{_datadir}/texmf/tex/latex/misc \ |
10fd38a7 JB |
126 | -datadir %{_datadir}/%{name} \ |
127 | -docdir %{_docdir}/%{name}-%{version} \ | |
128 | -libdir %{_libdir}/coq \ | |
129 | -mandir %{_mandir} \ | |
b2cb8983 | 130 | %if %{with ocaml_opt} |
b2cb8983 | 131 | -coqide opt \ |
10fd38a7 | 132 | -native-compiler yes \ |
b2cb8983 JR |
133 | %else |
134 | -byte-only \ | |
b2cb8983 | 135 | -coqide byte \ |
10fd38a7 | 136 | -native-compiler no \ |
b2cb8983 | 137 | %endif |
10fd38a7 JB |
138 | -browser "xdg-open %s" \ |
139 | %{?with_doc:-with-doc yes} | |
680764bb | 140 | |
b2cb8983 JR |
141 | %{__make} world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun |
142 | %{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories | |
680764bb JR |
143 | |
144 | %install | |
145 | rm -rf $RPM_BUILD_ROOT | |
8bee228d | 146 | install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} |
3432574d | 147 | |
b2cb8983 JR |
148 | %{__make} install \ |
149 | COQINSTALLPREFIX=$RPM_BUILD_ROOT%{_prefix} \ | |
150 | COQINSTALLPREFIX2=$RPM_BUILD_ROOT%{_sysconfdir} \ | |
151 | OLDROOT=%{_prefix} \ | |
152 | OLDROOT2=%{_sysconfdir} | |
153 | ||
680764bb JR |
154 | # To install only locally the binaries compiled with absolute paths |
155 | ||
b2cb8983 JR |
156 | cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} |
157 | cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} | |
8bee228d | 158 | |
10fd38a7 | 159 | cp -p CONTRIBUTING.md CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} |
c10c241b | 160 | |
680764bb JR |
161 | %clean |
162 | rm -rf $RPM_BUILD_ROOT | |
163 | ||
164 | %files | |
165 | %defattr(644,root,root,755) | |
c10c241b | 166 | %doc %{_docdir}/%{name}-%{version} |
650aa0b6 | 167 | %dir %{_sysconfdir}/%{name} |
680764bb | 168 | %attr(755,root,root) %{_bindir}/coqc |
2dc46485 | 169 | %attr(755,root,root) %{_bindir}/coqchk |
680764bb | 170 | %attr(755,root,root) %{_bindir}/coqdep |
1c74cbbc | 171 | %attr(755,root,root) %{_bindir}/coqdoc |
5f0acdc3 | 172 | %attr(755,root,root) %{_bindir}/coqide* |
b2cb8983 JR |
173 | %attr(755,root,root) %{_bindir}/coq_makefile |
174 | %attr(755,root,root) %{_bindir}/coqpp | |
175 | %attr(755,root,root) %{_bindir}/coqproofworker.opt | |
176 | %attr(755,root,root) %{_bindir}/coqqueryworker.opt | |
177 | %attr(755,root,root) %{_bindir}/coqtacticworker.opt | |
178 | %attr(755,root,root) %{_bindir}/coq-tex | |
861daf7b | 179 | %attr(755,root,root) %{_bindir}/coqtop |
b2cb8983 | 180 | %attr(755,root,root) %{_bindir}/coqtop.opt |
1c74cbbc | 181 | %attr(755,root,root) %{_bindir}/coqwc |
6b871b2b | 182 | %attr(755,root,root) %{_bindir}/coqworkmgr |
b2cb8983 JR |
183 | %attr(755,root,root) %{_bindir}/ocamllibdep |
184 | %attr(755,root,root) %{_bindir}/votour | |
3432574d | 185 | %dir %{_libdir}/coq |
1c74cbbc | 186 | %{_libdir}/coq/* |
9019ffc7 JR |
187 | %{_mandir}/man1/coq_makefile.1* |
188 | %{_mandir}/man1/coq-tex.1* | |
680764bb | 189 | %{_mandir}/man1/coqc.1* |
2dc46485 JR |
190 | %{_mandir}/man1/coqchk.1* |
191 | %{_mandir}/man1/coqdep.1* | |
192 | %{_mandir}/man1/coqdoc.1* | |
2dc46485 | 193 | %{_mandir}/man1/coqide.1* |
680764bb JR |
194 | %{_mandir}/man1/coqtop.1* |
195 | %{_mandir}/man1/coqtop.byte.1* | |
9e2234f9 | 196 | %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*} |
1c74cbbc | 197 | %{_mandir}/man1/coqwc.1* |
8bee228d JR |
198 | %{_desktopdir}/coqide.desktop |
199 | %{_pixmapsdir}/coqide.xpm | |
650aa0b6 | 200 | %{_datadir}/%{name} |
9019ffc7 | 201 | |
9019ffc7 JR |
202 | %files latex |
203 | %defattr(644,root,root,755) | |
204 | %{_datadir}/texmf/tex/latex/misc/coqdoc.sty |