- release 2 (by relup.sh)
[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
83437006 16Version: 8.4pl6
0e56eeba 17Release: 2
83437006 18License: LGPL v2.1
680764bb 19Group: Applications/Math
7f3d6db5 20Source0: http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz
83437006 21# Source0-md5: 2334a98b64578cb81d2b4127e327b368
8bee228d
JR
22Source1: coqide.desktop
23Source2: coqide.xpm
5f0acdc3 24Patch0: %{name}-lablgtk2.patch
3432574d 25URL: http://coq.inria.fr/
5f0acdc3 26BuildRequires: bash
680764bb 27BuildRequires: emacs
8bee228d
JR
28BuildRequires: hevea
29BuildRequires: netpbm-progs
861daf7b 30BuildRequires: ocaml >= 3.09.0
5f0acdc3 31BuildRequires: camlp5 >= 5.01
72eff188 32BuildRequires: ocaml-lablgtk2-devel >= 2.12.0
5f0acdc3 33BuildRequires: sed >= 4.0
9e2234f9 34BuildRequires: texlive-fonts-cmextra
83437006 35BuildRequires: texlive-fonts-cmsuper
9e2234f9 36BuildRequires: texlive-fonts-other
83437006 37BuildRequires: texlive-format-pdflatex
308e7511 38BuildRequires: texlive-latex-ams
8bee228d 39BuildRequires: texlive-latex-comment
b46eabb1 40BuildRequires: texlive-latex-moreverb
83437006
JB
41BuildRequires: texlive-latex-ucs
42BuildRequires: texlive-makeindex
8edb6738 43BuildRequires: texlive-psutils
83437006
JB
44# hyperref.sty (from latex) requires ifxexex.sty (from xetex)
45BuildRequires: texlive-xetex
f4499714 46%requires_eq ocaml-runtime
680764bb
JR
47BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
48
49%description
50Coq is a proof assistant which:
bcd66107 51 - allows to handle calculus assertions,
52 - check mechanically proofs of these assertions,
53 - helps to find formal proofs,
54 - extracts a certified program from the constructive proof of its
55 formal specification.
3432574d 56
3f4e388b
JR
57%description -l pl.UTF-8
58Coq to narzędzie pomagające w udowadnianiu, które:
59- pozwala uporać się z twierdzeniami dotyczącymi rachunku
60 różniczkowego,
61- mechanicznie sprawdzać dowody tych twierdzeń,
62- pomagać w znalezieniu formalnych dowodów,
63- wyciągać program o dowiedzionej poprawności z konstruktywnego
bcd66107 64 dowodu jego formalnej specyfikacji.
680764bb 65
9019ffc7
JR
66%package emacs
67Summary: Emacs mode and syntax for Coq
68Summary(pl.UTF-8): Tryb i składnia Coq dla Emacsa
69Group: Development/Tools
70Requires: %{name} = %{version}-%{release}
71
72%description emacs
73Emacs mode and suyntax files for Coq.
74
75%description emacs -l pl.UTF-8
76Pliki trybu i składni Coq dla Emacsa.
77
78%package latex
79Summary: Coq documentation style for latex
80Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa
81Group: Development/Tools
82Requires: %{name} = %{version}-%{release}
83
84%description latex
85Coq documentation style for latex.
86
87%description latex -l pl.UTF-8
88Styl dokumentacji Coq dla latexa.
89
680764bb
JR
90%prep
91%setup -q
5f0acdc3
JR
92%patch0 -p1
93
94%{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check
857e15b1 95%{__sed} -i -e 's|\(MAKE_TSOPTS=.*\) -s \(.*\)|\1 \2|' Makefile.build
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} \
680764bb 105 -emacs emacs \
8f33d8d4 106 -browser "xdg-open %s" \
680764bb 107 -emacslib %{_datadir}/emacs/site-lisp \
48226845 108 %{?with_ocaml_opt:-opt} \
1c74cbbc 109 --coqdocdir %{_datadir}/texmf/tex/latex/misc \
48226845 110 --coqide %{?with_ocaml_opt:opt}%{!?with_ocaml_opt:byte}
680764bb 111
48226845
JR
112%{__make} -j1 world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun
113%{?with_tests:%{__make} -j1 check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories
680764bb
JR
114
115%install
116rm -rf $RPM_BUILD_ROOT
8bee228d 117install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}}
3432574d
JB
118
119%{__make} -e install \
120 COQINSTALLPREFIX=$RPM_BUILD_ROOT/
680764bb
JR
121# To install only locally the binaries compiled with absolute paths
122
8bee228d
JR
123install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir}
124install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir}
125
c10c241b
JR
126# pdf is enough
127%{__rm} -r $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}/ps
83437006 128cp -p CHANGES COMPATIBILITY COPYRIGHT CREDITS README $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}
c10c241b 129
680764bb
JR
130%clean
131rm -rf $RPM_BUILD_ROOT
132
133%files
134%defattr(644,root,root,755)
c10c241b 135%doc %{_docdir}/%{name}-%{version}
650aa0b6
JR
136%dir %{_sysconfdir}/%{name}
137%config(noreplace) %verify(not md5 mtime size) %{_sysconfdir}/%{name}/coqide-gtk2rc
861daf7b 138%attr(755,root,root) %{_bindir}/coq_makefile
9019ffc7 139%attr(755,root,root) %{_bindir}/coq-tex
680764bb 140%attr(755,root,root) %{_bindir}/coqc
2dc46485 141%attr(755,root,root) %{_bindir}/coqchk
9e2234f9 142%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqchk.opt}
680764bb 143%attr(755,root,root) %{_bindir}/coqdep
1c74cbbc 144%attr(755,root,root) %{_bindir}/coqdoc
5f0acdc3 145%attr(755,root,root) %{_bindir}/coqide*
861daf7b
JR
146%attr(755,root,root) %{_bindir}/coqmktop
147%attr(755,root,root) %{_bindir}/coqtop
148%attr(755,root,root) %{_bindir}/coqtop.byte
9e2234f9 149%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqtop.opt}
1c74cbbc 150%attr(755,root,root) %{_bindir}/coqwc
861daf7b 151%attr(755,root,root) %{_bindir}/gallina
3432574d 152%dir %{_libdir}/coq
1c74cbbc 153%{_libdir}/coq/*
9019ffc7
JR
154%{_mandir}/man1/coq_makefile.1*
155%{_mandir}/man1/coq-tex.1*
680764bb 156%{_mandir}/man1/coqc.1*
2dc46485
JR
157%{_mandir}/man1/coqchk.1*
158%{_mandir}/man1/coqdep.1*
159%{_mandir}/man1/coqdoc.1*
2dc46485 160%{_mandir}/man1/coqide.1*
9019ffc7 161%{_mandir}/man1/coqmktop.1*
680764bb
JR
162%{_mandir}/man1/coqtop.1*
163%{_mandir}/man1/coqtop.byte.1*
9e2234f9 164%{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*}
1c74cbbc 165%{_mandir}/man1/coqwc.1*
2dc46485 166%{_mandir}/man1/gallina.1*
8bee228d
JR
167%{_desktopdir}/coqide.desktop
168%{_pixmapsdir}/coqide.xpm
650aa0b6 169%{_datadir}/%{name}
9019ffc7
JR
170
171%files emacs
172%defattr(644,root,root,755)
173%{_datadir}/emacs/site-lisp/coq.el
174%{_datadir}/emacs/site-lisp/coq-db.el
175%{_datadir}/emacs/site-lisp/coq-font-lock.el
176%{_datadir}/emacs/site-lisp/coq-inferior.el
177%{_datadir}/emacs/site-lisp/coq-syntax.el
178
179%files latex
180%defattr(644,root,root,755)
181%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
This page took 0.123751 seconds and 4 git commands to generate.