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