]> git.pld-linux.org Git - packages/coq.git/blame - coq.spec
- this version relies on fpmath=sse, so require sse2 on x86
[packages/coq.git] / coq.spec
CommitLineData
8f33d8d4
JR
1#
2# Conditional build:
10fd38a7 3%bcond_without ocaml_opt # native optimized binaries (bytecode is always built)
7b6fb8ed 4%bcond_without sse2 # SSE2 instructions (i387 maths not supported as of 8.15)
10fd38a7 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 16Summary: The Coq Proof Assistant
374d5475 17Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu
680764bb 18Name: coq
672cbc20
JB
19Version: 8.15.0
20Release: 1
83437006 21License: LGPL v2.1
680764bb 22Group: Applications/Math
672cbc20 23#Source0Download: https://github.com/coq/coq/releases
b2cb8983 24Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz
672cbc20 25# Source0-md5: cfa91d270e013b0ebe49120c2101d010
8bee228d
JR
26Source1: coqide.desktop
27Source2: coqide.xpm
672cbc20 28Patch0: %{name}-dune-prefix.patch
10fd38a7 29URL: https://coq.inria.fr/
5f0acdc3 30BuildRequires: bash
b2cb8983 31BuildRequires: ocaml >= 1:4.05
5f0acdc3 32BuildRequires: camlp5 >= 5.01
672cbc20 33BuildRequires: ocaml-dune >= 2.5.0
b2cb8983
JR
34BuildRequires: ocaml-findlib >= 1.8.1
35BuildRequires: ocaml-zarith-devel >= 1.10
10fd38a7
JB
36BuildRequires: ocaml-lablgtk3-devel >= 3.1.0
37BuildRequires: ocaml-lablgtk3-gtksourceview-devel >= 3.1.0
5f0acdc3 38BuildRequires: sed >= 4.0
10fd38a7
JB
39%if %{with doc}
40BuildRequires: python3 >= 1:3
41# TODO (and adjust package name)
42BuildRequires: python3-antlr4-python3-runtime >= 4.7.1
43BuildRequires: python3-bs4 >= 4.0.6
44BuildRequires: python3-pexpect >= 4.2.1
45BuildRequires: python3-sphinx_rtd_theme >= 0.4.3
46# TODO (and adjust package name)
47BuildRequires: python3-sphinxcontrib-bibtex >= 0.4.2
48BuildRequires: sphinx-pdg >= 2.3.1
49# TODO: update texlive packages list (or drop pdf building leaving only html)
9e2234f9 50BuildRequires: texlive-fonts-cmextra
83437006 51BuildRequires: texlive-fonts-cmsuper
9e2234f9 52BuildRequires: texlive-fonts-other
83437006 53BuildRequires: texlive-format-pdflatex
308e7511 54BuildRequires: texlive-latex-ams
8bee228d 55BuildRequires: texlive-latex-comment
b46eabb1 56BuildRequires: texlive-latex-moreverb
83437006
JB
57BuildRequires: texlive-latex-ucs
58BuildRequires: texlive-makeindex
8edb6738 59BuildRequires: texlive-psutils
83437006
JB
60# hyperref.sty (from latex) requires ifxexex.sty (from xetex)
61BuildRequires: texlive-xetex
10fd38a7
JB
62%endif
63%if %{with sse2}
64Requires: cpuinfo(sse2)
65%endif
672cbc20 66Requires: ocaml-coq-devel = %{version}-%{release}
b2cb8983 67Obsoletes: coq-emacs < 8.13.1
3e0583a4 68# same as ocaml-zarith
39bb0263 69ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
680764bb
JR
70BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
71
3809f5df
JR
72# Exclude private ocaml interfaces
73%define _noautoreq ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\)
74
680764bb
JR
75%description
76Coq is a proof assistant which:
bcd66107 77 - allows to handle calculus assertions,
78 - check mechanically proofs of these assertions,
79 - helps to find formal proofs,
80 - extracts a certified program from the constructive proof of its
81 formal specification.
3432574d 82
3f4e388b
JR
83%description -l pl.UTF-8
84Coq to narzędzie pomagające w udowadnianiu, które:
85- pozwala uporać się z twierdzeniami dotyczącymi rachunku
86 różniczkowego,
87- mechanicznie sprawdzać dowody tych twierdzeń,
88- pomagać w znalezieniu formalnych dowodów,
b2cb8983
JR
89- wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu
90 jego formalnej specyfikacji.
9019ffc7 91
672cbc20
JB
92%package -n ocaml-coq
93Summary: Coq Proof Assistant - OCaml runtime libraries
94Summary(pl.UTF-8): Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla
95Group: Libraries
96%requires_eq ocaml-runtime
97
98%description -n ocaml-coq
99Coq Proof Assistant - OCaml runtime libraries.
100
101%description -n ocaml-coq -l pl.UTF-8
102Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla.
103
104%package -n ocaml-coq-devel
105Summary: Coq Proof Assistant - OCaml development libraries
106Summary(pl.UTF-8): Asystent udowadniania Coq - biblioteki programistyczne OCamla
107Group: Development/Libraries
108Requires: ocaml-coq = %{version}-%{release}
109%requires_eq ocaml
110
111%description -n ocaml-coq-devel
112Coq Proof Assistant - OCaml development libraries.
113
114%description -n ocaml-coq-devel -l pl.UTF-8
115Asystent udowadniania Coq - biblioteki programistyczne OCamla.
116
9019ffc7 117%package latex
10fd38a7
JB
118Summary: Coq documentation style for LaTeX
119Summary(pl.UTF-8): Styl dokumentacji Coq dla LaTeXa
9019ffc7
JR
120Group: Development/Tools
121Requires: %{name} = %{version}-%{release}
122
123%description latex
10fd38a7 124Coq documentation style for LaTeX.
9019ffc7
JR
125
126%description latex -l pl.UTF-8
10fd38a7 127Styl dokumentacji Coq dla LaTeXa.
9019ffc7 128
680764bb
JR
129%prep
130%setup -q
672cbc20 131%patch0 -p1
5f0acdc3 132
672cbc20 133%{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' tools/configure/configure.ml
e041a8de
JB
134%if %{without sse2}
135%{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' tools/configure/configure.ml
10fd38a7 136%endif
672cbc20 137%{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in
b2cb8983 138
672cbc20 139%{__sed} -i -e '1s,/usr/bin/env python3,%{__python3},' \
b2cb8983
JR
140 tools/make-both-single-timing-files.py \
141 tools/make-both-time-files.py \
142 tools/make-one-time-file.py
143
672cbc20 144%{__sed} -i -e '1s,/usr/bin/env python2,%{__python3},' \
b2cb8983 145 doc/tools/coqrst/notations/fontsupport.py
680764bb
JR
146
147%build
148./configure \
672cbc20 149 -prefix %{_prefix} \
650aa0b6 150 -configdir %{_sysconfdir}/%{name} \
10fd38a7
JB
151 -datadir %{_datadir}/%{name} \
152 -docdir %{_docdir}/%{name}-%{version} \
153 -libdir %{_libdir}/coq \
154 -mandir %{_mandir} \
b2cb8983 155%if %{with ocaml_opt}
b2cb8983 156 -coqide opt \
10fd38a7 157 -native-compiler yes \
b2cb8983
JR
158%else
159 -byte-only \
b2cb8983 160 -coqide byte \
10fd38a7 161 -native-compiler no \
b2cb8983 162%endif
10fd38a7
JB
163 -browser "xdg-open %s" \
164 %{?with_doc:-with-doc yes}
680764bb 165
672cbc20
JB
166%{__make} world \
167 CAML_LD_LIBRARY_PATH=kernel/byterun \
168 _DDISPLAY=verbose \
169 VERBOSE=1
b2cb8983 170%{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories
680764bb
JR
171
172%install
173rm -rf $RPM_BUILD_ROOT
672cbc20 174install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir},%{_sysconfdir}/%{name}}
3432574d 175
b2cb8983 176%{__make} install \
672cbc20
JB
177 _DDISPLAY=verbose \
178 DESTDIR=$RPM_BUILD_ROOT
680764bb 179
b2cb8983
JR
180cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir}
181cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir}
8bee228d 182
672cbc20
JB
183cp -p CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}
184
185%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*.ml
186%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*.ml
187%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*/*.ml
188%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coqide-server/*/*.ml
189# build time
190%{__rm} -r $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/tools
c10c241b 191
680764bb
JR
192%clean
193rm -rf $RPM_BUILD_ROOT
194
195%files
196%defattr(644,root,root,755)
c10c241b 197%doc %{_docdir}/%{name}-%{version}
650aa0b6 198%dir %{_sysconfdir}/%{name}
672cbc20
JB
199%attr(755,root,root) %{_bindir}/coq-tex
200%attr(755,root,root) %{_bindir}/coq_makefile
680764bb 201%attr(755,root,root) %{_bindir}/coqc
672cbc20 202%attr(755,root,root) %{_bindir}/coqc.byte
2dc46485 203%attr(755,root,root) %{_bindir}/coqchk
680764bb 204%attr(755,root,root) %{_bindir}/coqdep
1c74cbbc 205%attr(755,root,root) %{_bindir}/coqdoc
672cbc20
JB
206%attr(755,root,root) %{_bindir}/coqide
207%attr(755,root,root) %{_bindir}/coqidetop.byte
208%attr(755,root,root) %{_bindir}/coqidetop.opt
209%attr(755,root,root) %{_bindir}/coqnative
b2cb8983
JR
210%attr(755,root,root) %{_bindir}/coqpp
211%attr(755,root,root) %{_bindir}/coqproofworker.opt
212%attr(755,root,root) %{_bindir}/coqqueryworker.opt
213%attr(755,root,root) %{_bindir}/coqtacticworker.opt
861daf7b 214%attr(755,root,root) %{_bindir}/coqtop
672cbc20 215%attr(755,root,root) %{_bindir}/coqtop.byte
b2cb8983 216%attr(755,root,root) %{_bindir}/coqtop.opt
1c74cbbc 217%attr(755,root,root) %{_bindir}/coqwc
6b871b2b 218%attr(755,root,root) %{_bindir}/coqworkmgr
672cbc20 219%attr(755,root,root) %{_bindir}/csdpcert
b2cb8983
JR
220%attr(755,root,root) %{_bindir}/ocamllibdep
221%attr(755,root,root) %{_bindir}/votour
3432574d 222%dir %{_libdir}/coq
672cbc20
JB
223%{_libdir}/coq/theories
224%{_libdir}/coq/user-contrib
9019ffc7
JR
225%{_mandir}/man1/coq_makefile.1*
226%{_mandir}/man1/coq-tex.1*
680764bb 227%{_mandir}/man1/coqc.1*
2dc46485
JR
228%{_mandir}/man1/coqchk.1*
229%{_mandir}/man1/coqdep.1*
230%{_mandir}/man1/coqdoc.1*
2dc46485 231%{_mandir}/man1/coqide.1*
672cbc20 232%{_mandir}/man1/coqnative.1*
680764bb
JR
233%{_mandir}/man1/coqtop.1*
234%{_mandir}/man1/coqtop.byte.1*
9e2234f9 235%{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*}
1c74cbbc 236%{_mandir}/man1/coqwc.1*
8bee228d
JR
237%{_desktopdir}/coqide.desktop
238%{_pixmapsdir}/coqide.xpm
650aa0b6 239%{_datadir}/%{name}
9019ffc7 240
672cbc20
JB
241%files -n ocaml-coq
242%defattr(644,root,root,755)
243%dir %{_libdir}/ocaml/coq-core
244%{_libdir}/ocaml/coq-core/META
245%{_libdir}/ocaml/coq-core/revision
246%dir %{_libdir}/ocaml/coq-core/boot
247%{_libdir}/ocaml/coq-core/boot/*.cma
248%dir %{_libdir}/ocaml/coq-core/clib
249%{_libdir}/ocaml/coq-core/clib/*.cma
250%dir %{_libdir}/ocaml/coq-core/config
251%{_libdir}/ocaml/coq-core/config/*.cma
252%dir %{_libdir}/ocaml/coq-core/engine
253%{_libdir}/ocaml/coq-core/engine/*.cma
254%dir %{_libdir}/ocaml/coq-core/gramlib
255%{_libdir}/ocaml/coq-core/gramlib/*.cma
256%dir %{_libdir}/ocaml/coq-core/interp
257%{_libdir}/ocaml/coq-core/interp/*.cma
258%dir %{_libdir}/ocaml/coq-core/kernel
259%{_libdir}/ocaml/coq-core/kernel/*.cma
260%dir %{_libdir}/ocaml/coq-core/lib
261%{_libdir}/ocaml/coq-core/lib/*.cma
262%dir %{_libdir}/ocaml/coq-core/library
263%{_libdir}/ocaml/coq-core/library/*.cma
264%dir %{_libdir}/ocaml/coq-core/parsing
265%{_libdir}/ocaml/coq-core/parsing/*.cma
266%dir %{_libdir}/ocaml/coq-core/plugins
267%dir %{_libdir}/ocaml/coq-core/plugins/btauto
268%{_libdir}/ocaml/coq-core/plugins/btauto/*.cma
269%dir %{_libdir}/ocaml/coq-core/plugins/cc
270%{_libdir}/ocaml/coq-core/plugins/cc/*.cma
271%dir %{_libdir}/ocaml/coq-core/plugins/derive
272%{_libdir}/ocaml/coq-core/plugins/derive/*.cma
273%dir %{_libdir}/ocaml/coq-core/plugins/extraction
274%{_libdir}/ocaml/coq-core/plugins/extraction/*.cma
275%dir %{_libdir}/ocaml/coq-core/plugins/firstorder
276%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cma
277%dir %{_libdir}/ocaml/coq-core/plugins/funind
278%{_libdir}/ocaml/coq-core/plugins/funind/*.cma
279%dir %{_libdir}/ocaml/coq-core/plugins/ltac
280%{_libdir}/ocaml/coq-core/plugins/ltac/*.cma
281%dir %{_libdir}/ocaml/coq-core/plugins/ltac2
282%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cma
283%dir %{_libdir}/ocaml/coq-core/plugins/micromega
284%{_libdir}/ocaml/coq-core/plugins/micromega/*.cma
285%dir %{_libdir}/ocaml/coq-core/plugins/nsatz
286%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cma
287%dir %{_libdir}/ocaml/coq-core/plugins/number_string_notation
288%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cma
289%dir %{_libdir}/ocaml/coq-core/plugins/ring
290%{_libdir}/ocaml/coq-core/plugins/ring/*.cma
291%dir %{_libdir}/ocaml/coq-core/plugins/rtauto
292%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cma
293%dir %{_libdir}/ocaml/coq-core/plugins/ssreflect
294%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cma
295%dir %{_libdir}/ocaml/coq-core/plugins/ssrmatching
296%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cma
297%dir %{_libdir}/ocaml/coq-core/plugins/tauto
298%{_libdir}/ocaml/coq-core/plugins/tauto/*.cma
299%dir %{_libdir}/ocaml/coq-core/plugins/tutorial
300%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p0
301%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cma
302%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p1
303%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cma
304%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p2
305%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cma
306%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p3
307%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cma
308%dir %{_libdir}/ocaml/coq-core/plugins/zify
309%{_libdir}/ocaml/coq-core/plugins/zify/*.cma
310%dir %{_libdir}/ocaml/coq-core/pretyping
311%{_libdir}/ocaml/coq-core/pretyping/*.cma
312%dir %{_libdir}/ocaml/coq-core/printing
313%{_libdir}/ocaml/coq-core/printing/*.cma
314%dir %{_libdir}/ocaml/coq-core/proofs
315%{_libdir}/ocaml/coq-core/proofs/*.cma
316%dir %{_libdir}/ocaml/coq-core/stm
317%{_libdir}/ocaml/coq-core/stm/*.cma
318%dir %{_libdir}/ocaml/coq-core/sysinit
319%{_libdir}/ocaml/coq-core/sysinit/*.cma
320%dir %{_libdir}/ocaml/coq-core/tactics
321%{_libdir}/ocaml/coq-core/tactics/*.cma
322%dir %{_libdir}/ocaml/coq-core/top_printers
323%{_libdir}/ocaml/coq-core/top_printers/*.cma
324%dir %{_libdir}/ocaml/coq-core/toplevel
325%{_libdir}/ocaml/coq-core/toplevel/*.cma
326%dir %{_libdir}/ocaml/coq-core/vernac
327%{_libdir}/ocaml/coq-core/vernac/*.cma
328%dir %{_libdir}/ocaml/coq-core/vm
329%{_libdir}/ocaml/coq-core/vm/*.cma
330%dir %{_libdir}/ocaml/coqide
331%{_libdir}/ocaml/coqide/META
332%dir %{_libdir}/ocaml/coqide-server
333%{_libdir}/ocaml/coqide-server/META
334%dir %{_libdir}/ocaml/coqide-server/core
335%{_libdir}/ocaml/coqide-server/core/*.cma
336%dir %{_libdir}/ocaml/coqide-server/protocol
337%{_libdir}/ocaml/coqide-server/protocol/*.cma
338%if %{with ocaml_opt}
339%attr(755,root,root) %{_libdir}/ocaml/coq-core/boot/*.cmxs
340%attr(755,root,root) %{_libdir}/ocaml/coq-core/clib/*.cmxs
341%attr(755,root,root) %{_libdir}/ocaml/coq-core/config/*.cmxs
342%attr(755,root,root) %{_libdir}/ocaml/coq-core/engine/*.cmxs
343%attr(755,root,root) %{_libdir}/ocaml/coq-core/gramlib/*.cmxs
344%attr(755,root,root) %{_libdir}/ocaml/coq-core/interp/*.cmxs
345%attr(755,root,root) %{_libdir}/ocaml/coq-core/kernel/*.cmxs
346%attr(755,root,root) %{_libdir}/ocaml/coq-core/lib/*.cmxs
347%attr(755,root,root) %{_libdir}/ocaml/coq-core/library/*.cmxs
348%attr(755,root,root) %{_libdir}/ocaml/coq-core/parsing/*.cmxs
349%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxs
350%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/cc/*.cmxs
351%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/derive/*.cmxs
352%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxs
353%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxs
354%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/funind/*.cmxs
355%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxs
356%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxs
357%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxs
358%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxs
359%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxs
360%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ring/*.cmxs
361%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxs
362%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxs
363%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxs
364%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxs
365%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxs
366%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxs
367%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxs
368%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxs
369%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/zify/*.cmxs
370%attr(755,root,root) %{_libdir}/ocaml/coq-core/pretyping/*.cmxs
371%attr(755,root,root) %{_libdir}/ocaml/coq-core/printing/*.cmxs
372%attr(755,root,root) %{_libdir}/ocaml/coq-core/proofs/*.cmxs
373%attr(755,root,root) %{_libdir}/ocaml/coq-core/stm/*.cmxs
374%attr(755,root,root) %{_libdir}/ocaml/coq-core/sysinit/*.cmxs
375%attr(755,root,root) %{_libdir}/ocaml/coq-core/tactics/*.cmxs
376%attr(755,root,root) %{_libdir}/ocaml/coq-core/top_printers/*.cmxs
377%attr(755,root,root) %{_libdir}/ocaml/coq-core/toplevel/*.cmxs
378%attr(755,root,root) %{_libdir}/ocaml/coq-core/vernac/*.cmxs
379%attr(755,root,root) %{_libdir}/ocaml/coq-core/vm/*.cmxs
380%attr(755,root,root) %{_libdir}/ocaml/coqide-server/core/*.cmxs
381%attr(755,root,root) %{_libdir}/ocaml/coqide-server/protocol/*.cmxs
382%endif
383%attr(755,root,root) %{_libdir}/ocaml/stublibs/dllcoqrun_stubs.so
384
385%files -n ocaml-coq-devel
386%defattr(644,root,root,755)
387%{_libdir}/ocaml/coq-core/dune-package
388%{_libdir}/ocaml/coq-core/opam
389%{_libdir}/ocaml/coq-core/boot/*.cmi
390%{_libdir}/ocaml/coq-core/boot/*.cmt
391%{_libdir}/ocaml/coq-core/boot/*.cmti
392%{_libdir}/ocaml/coq-core/boot/*.mli
393%{_libdir}/ocaml/coq-core/clib/*.cmi
394%{_libdir}/ocaml/coq-core/clib/*.cmt
395%{_libdir}/ocaml/coq-core/clib/*.cmti
396%{_libdir}/ocaml/coq-core/clib/*.mli
397%{_libdir}/ocaml/coq-core/config/*.cmi
398%{_libdir}/ocaml/coq-core/config/*.cmt
399%{_libdir}/ocaml/coq-core/config/*.cmti
400%{_libdir}/ocaml/coq-core/config/*.mli
401%{_libdir}/ocaml/coq-core/engine/*.cmi
402%{_libdir}/ocaml/coq-core/engine/*.cmt
403%{_libdir}/ocaml/coq-core/engine/*.cmti
404%{_libdir}/ocaml/coq-core/engine/*.mli
405%{_libdir}/ocaml/coq-core/gramlib/*.cmi
406%{_libdir}/ocaml/coq-core/gramlib/*.cmt
407%{_libdir}/ocaml/coq-core/gramlib/*.cmti
408%{_libdir}/ocaml/coq-core/gramlib/*.mli
409%{_libdir}/ocaml/coq-core/interp/*.cmi
410%{_libdir}/ocaml/coq-core/interp/*.cmt
411%{_libdir}/ocaml/coq-core/interp/*.cmti
412%{_libdir}/ocaml/coq-core/interp/*.mli
413%{_libdir}/ocaml/coq-core/kernel/*.cmi
414%{_libdir}/ocaml/coq-core/kernel/*.cmt
415%{_libdir}/ocaml/coq-core/kernel/*.cmti
416%{_libdir}/ocaml/coq-core/kernel/*.mli
417%{_libdir}/ocaml/coq-core/lib/*.cmi
418%{_libdir}/ocaml/coq-core/lib/*.cmt
419%{_libdir}/ocaml/coq-core/lib/*.cmti
420%{_libdir}/ocaml/coq-core/lib/*.mli
421%{_libdir}/ocaml/coq-core/library/*.cmi
422%{_libdir}/ocaml/coq-core/library/*.cmt
423%{_libdir}/ocaml/coq-core/library/*.cmti
424%{_libdir}/ocaml/coq-core/library/*.mli
425%{_libdir}/ocaml/coq-core/parsing/*.cmi
426%{_libdir}/ocaml/coq-core/parsing/*.cmt
427%{_libdir}/ocaml/coq-core/parsing/*.cmti
428%{_libdir}/ocaml/coq-core/parsing/*.mli
429%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmi
430%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmt
431%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmti
432%{_libdir}/ocaml/coq-core/plugins/btauto/*.mli
433%{_libdir}/ocaml/coq-core/plugins/cc/*.cmi
434%{_libdir}/ocaml/coq-core/plugins/cc/*.cmt
435%{_libdir}/ocaml/coq-core/plugins/cc/*.cmti
436%{_libdir}/ocaml/coq-core/plugins/cc/*.mli
437%{_libdir}/ocaml/coq-core/plugins/derive/*.cmi
438%{_libdir}/ocaml/coq-core/plugins/derive/*.cmt
439%{_libdir}/ocaml/coq-core/plugins/derive/*.cmti
440%{_libdir}/ocaml/coq-core/plugins/derive/*.mli
441%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmi
442%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmt
443%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmti
444%{_libdir}/ocaml/coq-core/plugins/extraction/*.mli
445%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmi
446%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmt
447%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmti
448%{_libdir}/ocaml/coq-core/plugins/firstorder/*.mli
449%{_libdir}/ocaml/coq-core/plugins/funind/*.cmi
450%{_libdir}/ocaml/coq-core/plugins/funind/*.cmt
451%{_libdir}/ocaml/coq-core/plugins/funind/*.cmti
452%{_libdir}/ocaml/coq-core/plugins/funind/*.mli
453%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmi
454%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmt
455%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmti
456%{_libdir}/ocaml/coq-core/plugins/ltac/*.mli
457%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmi
458%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmt
459%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmti
460%{_libdir}/ocaml/coq-core/plugins/ltac2/*.mli
461%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmi
462%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmt
463%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmti
464%{_libdir}/ocaml/coq-core/plugins/micromega/*.mli
465%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmi
466%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmt
467%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmti
468%{_libdir}/ocaml/coq-core/plugins/nsatz/*.mli
469%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmi
470%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmt
471%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmti
472%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.mli
473%{_libdir}/ocaml/coq-core/plugins/ring/*.cmi
474%{_libdir}/ocaml/coq-core/plugins/ring/*.cmt
475%{_libdir}/ocaml/coq-core/plugins/ring/*.cmti
476%{_libdir}/ocaml/coq-core/plugins/ring/*.mli
477%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmi
478%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmt
479%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmti
480%{_libdir}/ocaml/coq-core/plugins/rtauto/*.mli
481%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmi
482%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmt
483%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmti
484%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.mli
485%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmi
486%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmt
487%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmti
488%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.mli
489%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmi
490%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmt
491%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmti
492%{_libdir}/ocaml/coq-core/plugins/tauto/*.mli
493%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmi
494%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmt
495%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmti
496%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.mli
497%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmi
498%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmt
499%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmti
500%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.mli
501%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmi
502%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmt
503%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmti
504%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.mli
505%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmi
506%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmt
507%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmti
508%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.mli
509%{_libdir}/ocaml/coq-core/plugins/zify/*.cmi
510%{_libdir}/ocaml/coq-core/plugins/zify/*.cmt
511%{_libdir}/ocaml/coq-core/plugins/zify/*.cmti
512%{_libdir}/ocaml/coq-core/plugins/zify/*.mli
513%{_libdir}/ocaml/coq-core/pretyping/*.cmi
514%{_libdir}/ocaml/coq-core/pretyping/*.cmt
515%{_libdir}/ocaml/coq-core/pretyping/*.cmti
516%{_libdir}/ocaml/coq-core/pretyping/*.mli
517%{_libdir}/ocaml/coq-core/printing/*.cmi
518%{_libdir}/ocaml/coq-core/printing/*.cmt
519%{_libdir}/ocaml/coq-core/printing/*.cmti
520%{_libdir}/ocaml/coq-core/printing/*.mli
521%{_libdir}/ocaml/coq-core/proofs/*.cmi
522%{_libdir}/ocaml/coq-core/proofs/*.cmt
523%{_libdir}/ocaml/coq-core/proofs/*.cmti
524%{_libdir}/ocaml/coq-core/proofs/*.mli
525%{_libdir}/ocaml/coq-core/stm/*.cmi
526%{_libdir}/ocaml/coq-core/stm/*.cmt
527%{_libdir}/ocaml/coq-core/stm/*.cmti
528%{_libdir}/ocaml/coq-core/stm/*.mli
529%{_libdir}/ocaml/coq-core/sysinit/*.cmi
530%{_libdir}/ocaml/coq-core/sysinit/*.cmt
531%{_libdir}/ocaml/coq-core/sysinit/*.cmti
532%{_libdir}/ocaml/coq-core/sysinit/*.mli
533%{_libdir}/ocaml/coq-core/tactics/*.cmi
534%{_libdir}/ocaml/coq-core/tactics/*.cmt
535%{_libdir}/ocaml/coq-core/tactics/*.cmti
536%{_libdir}/ocaml/coq-core/tactics/*.mli
537%{_libdir}/ocaml/coq-core/top_printers/*.cmi
538%{_libdir}/ocaml/coq-core/top_printers/*.cmt
539%{_libdir}/ocaml/coq-core/top_printers/*.cmti
540%{_libdir}/ocaml/coq-core/top_printers/*.mli
541%{_libdir}/ocaml/coq-core/toplevel/*.cmi
542%{_libdir}/ocaml/coq-core/toplevel/*.cmt
543%{_libdir}/ocaml/coq-core/toplevel/*.cmti
544%{_libdir}/ocaml/coq-core/toplevel/*.mli
545%{_libdir}/ocaml/coq-core/vernac/*.cmi
546%{_libdir}/ocaml/coq-core/vernac/*.cmt
547%{_libdir}/ocaml/coq-core/vernac/*.cmti
548%{_libdir}/ocaml/coq-core/vernac/*.mli
549%{_libdir}/ocaml/coq-core/vm/libcoqrun_stubs.a
550%{_libdir}/ocaml/coq-core/vm/*.cmi
551%{_libdir}/ocaml/coq-core/vm/*.cmt
552%{_libdir}/ocaml/coqide/dune-package
553%{_libdir}/ocaml/coqide/opam
554%{_libdir}/ocaml/coqide-server/dune-package
555%{_libdir}/ocaml/coqide-server/opam
556%{_libdir}/ocaml/coqide-server/core/*.cmi
557%{_libdir}/ocaml/coqide-server/core/*.cmt
558%{_libdir}/ocaml/coqide-server/core/*.cmti
559%{_libdir}/ocaml/coqide-server/core/*.mli
560%{_libdir}/ocaml/coqide-server/protocol/*.cmi
561%{_libdir}/ocaml/coqide-server/protocol/*.cmt
562%{_libdir}/ocaml/coqide-server/protocol/*.cmti
563%{_libdir}/ocaml/coqide-server/protocol/*.mli
564%if %{with ocaml_opt}
565%{_libdir}/ocaml/coq-core/boot/boot.a
566%{_libdir}/ocaml/coq-core/boot/*.cmx
567%{_libdir}/ocaml/coq-core/boot/*.cmxa
568%{_libdir}/ocaml/coq-core/clib/clib.a
569%{_libdir}/ocaml/coq-core/clib/*.cmx
570%{_libdir}/ocaml/coq-core/clib/*.cmxa
571%{_libdir}/ocaml/coq-core/config/config.a
572%{_libdir}/ocaml/coq-core/config/*.cmx
573%{_libdir}/ocaml/coq-core/config/*.cmxa
574%{_libdir}/ocaml/coq-core/engine/engine.a
575%{_libdir}/ocaml/coq-core/engine/*.cmx
576%{_libdir}/ocaml/coq-core/engine/*.cmxa
577%{_libdir}/ocaml/coq-core/gramlib/gramlib.a
578%{_libdir}/ocaml/coq-core/gramlib/*.cmx
579%{_libdir}/ocaml/coq-core/gramlib/*.cmxa
580%{_libdir}/ocaml/coq-core/interp/interp.a
581%{_libdir}/ocaml/coq-core/interp/*.cmx
582%{_libdir}/ocaml/coq-core/interp/*.cmxa
583%{_libdir}/ocaml/coq-core/kernel/kernel.a
584%{_libdir}/ocaml/coq-core/kernel/*.cmx
585%{_libdir}/ocaml/coq-core/kernel/*.cmxa
586%{_libdir}/ocaml/coq-core/lib/lib.a
587%{_libdir}/ocaml/coq-core/lib/*.cmx
588%{_libdir}/ocaml/coq-core/lib/*.cmxa
589%{_libdir}/ocaml/coq-core/library/library.a
590%{_libdir}/ocaml/coq-core/library/*.cmx
591%{_libdir}/ocaml/coq-core/library/*.cmxa
592%{_libdir}/ocaml/coq-core/parsing/parsing.a
593%{_libdir}/ocaml/coq-core/parsing/*.cmx
594%{_libdir}/ocaml/coq-core/parsing/*.cmxa
595%{_libdir}/ocaml/coq-core/plugins/btauto/btauto_plugin.a
596%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmx
597%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxa
598%{_libdir}/ocaml/coq-core/plugins/cc/cc_plugin.a
599%{_libdir}/ocaml/coq-core/plugins/cc/*.cmx
600%{_libdir}/ocaml/coq-core/plugins/cc/*.cmxa
601%{_libdir}/ocaml/coq-core/plugins/derive/derive_plugin.a
602%{_libdir}/ocaml/coq-core/plugins/derive/*.cmx
603%{_libdir}/ocaml/coq-core/plugins/derive/*.cmxa
604%{_libdir}/ocaml/coq-core/plugins/extraction/extraction_plugin.a
605%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmx
606%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxa
607%{_libdir}/ocaml/coq-core/plugins/firstorder/firstorder_plugin.a
608%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmx
609%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxa
610%{_libdir}/ocaml/coq-core/plugins/funind/funind_plugin.a
611%{_libdir}/ocaml/coq-core/plugins/funind/*.cmx
612%{_libdir}/ocaml/coq-core/plugins/funind/*.cmxa
613%{_libdir}/ocaml/coq-core/plugins/ltac/ltac_plugin.a
614%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmx
615%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxa
616%{_libdir}/ocaml/coq-core/plugins/ltac2/ltac2_plugin.a
617%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmx
618%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxa
619%{_libdir}/ocaml/coq-core/plugins/micromega/micromega_plugin.a
620%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmx
621%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxa
622%{_libdir}/ocaml/coq-core/plugins/nsatz/nsatz_plugin.a
623%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmx
624%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxa
625%{_libdir}/ocaml/coq-core/plugins/number_string_notation/number_string_notation_plugin.a
626%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmx
627%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxa
628%{_libdir}/ocaml/coq-core/plugins/ring/ring_plugin.a
629%{_libdir}/ocaml/coq-core/plugins/ring/*.cmx
630%{_libdir}/ocaml/coq-core/plugins/ring/*.cmxa
631%{_libdir}/ocaml/coq-core/plugins/rtauto/rtauto_plugin.a
632%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmx
633%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxa
634%{_libdir}/ocaml/coq-core/plugins/ssreflect/ssreflect_plugin.a
635%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmx
636%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxa
637%{_libdir}/ocaml/coq-core/plugins/ssrmatching/ssrmatching_plugin.a
638%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmx
639%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxa
640%{_libdir}/ocaml/coq-core/plugins/tauto/tauto_plugin.a
641%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmx
642%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxa
643%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/tuto0_plugin.a
644%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmx
645%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxa
646%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/tuto1_plugin.a
647%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmx
648%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxa
649%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/tuto2_plugin.a
650%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmx
651%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxa
652%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/tuto3_plugin.a
653%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmx
654%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxa
655%{_libdir}/ocaml/coq-core/plugins/zify/zify_plugin.a
656%{_libdir}/ocaml/coq-core/plugins/zify/*.cmx
657%{_libdir}/ocaml/coq-core/plugins/zify/*.cmxa
658%{_libdir}/ocaml/coq-core/pretyping/pretyping.a
659%{_libdir}/ocaml/coq-core/pretyping/*.cmx
660%{_libdir}/ocaml/coq-core/pretyping/*.cmxa
661%{_libdir}/ocaml/coq-core/printing/printing.a
662%{_libdir}/ocaml/coq-core/printing/*.cmx
663%{_libdir}/ocaml/coq-core/printing/*.cmxa
664%{_libdir}/ocaml/coq-core/proofs/proofs.a
665%{_libdir}/ocaml/coq-core/proofs/*.cmx
666%{_libdir}/ocaml/coq-core/proofs/*.cmxa
667%{_libdir}/ocaml/coq-core/stm/stm.a
668%{_libdir}/ocaml/coq-core/stm/*.cmx
669%{_libdir}/ocaml/coq-core/stm/*.cmxa
670%{_libdir}/ocaml/coq-core/sysinit/sysinit.a
671%{_libdir}/ocaml/coq-core/sysinit/*.cmx
672%{_libdir}/ocaml/coq-core/sysinit/*.cmxa
673%{_libdir}/ocaml/coq-core/tactics/tactics.a
674%{_libdir}/ocaml/coq-core/tactics/*.cmx
675%{_libdir}/ocaml/coq-core/tactics/*.cmxa
676%{_libdir}/ocaml/coq-core/top_printers/top_printers.a
677%{_libdir}/ocaml/coq-core/top_printers/*.cmx
678%{_libdir}/ocaml/coq-core/top_printers/*.cmxa
679%{_libdir}/ocaml/coq-core/toplevel/toplevel.a
680%{_libdir}/ocaml/coq-core/toplevel/*.cmx
681%{_libdir}/ocaml/coq-core/toplevel/*.cmxa
682%{_libdir}/ocaml/coq-core/vernac/vernac.a
683%{_libdir}/ocaml/coq-core/vernac/*.cmx
684%{_libdir}/ocaml/coq-core/vernac/*.cmxa
685%{_libdir}/ocaml/coq-core/vm/coqrun.a
686%{_libdir}/ocaml/coq-core/vm/*.cmx
687%{_libdir}/ocaml/coq-core/vm/*.cmxa
688%{_libdir}/ocaml/coqide-server/core/core.a
689%{_libdir}/ocaml/coqide-server/core/*.cmx
690%{_libdir}/ocaml/coqide-server/core/*.cmxa
691%{_libdir}/ocaml/coqide-server/protocol/protocol.a
692%{_libdir}/ocaml/coqide-server/protocol/*.cmx
693%{_libdir}/ocaml/coqide-server/protocol/*.cmxa
694%endif
695
9019ffc7
JR
696%files latex
697%defattr(644,root,root,755)
698%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
This page took 0.279515 seconds and 4 git commands to generate.