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