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