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