- TODO and proper explanation why tests fail
[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
72eff188 11Version: 8.3pl1
8bee228d 12Release: 0.1
680764bb
JR
13License: GPL
14Group: Applications/Math
15Vendor: INRIA Rocquencourt
5f0acdc3 16Source0: http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz
72eff188 17# Source0-md5: 1869d22b337f5da59ba3bbe1433f9a3b
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
680764bb
JR
35BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
36
37%description
38Coq is a proof assistant which:
bcd66107 39 - allows to handle calculus assertions,
40 - check mechanically proofs of these assertions,
41 - helps to find formal proofs,
42 - extracts a certified program from the constructive proof of its
43 formal specification.
3432574d 44
3f4e388b
JR
45%description -l pl.UTF-8
46Coq to narzędzie pomagające w udowadnianiu, które:
47- pozwala uporać się z twierdzeniami dotyczącymi rachunku
48 różniczkowego,
49- mechanicznie sprawdzać dowody tych twierdzeń,
50- pomagać w znalezieniu formalnych dowodów,
51- wyciągać program o dowiedzionej poprawności z konstruktywnego
bcd66107 52 dowodu jego formalnej specyfikacji.
680764bb 53
9019ffc7
JR
54%package emacs
55Summary: Emacs mode and syntax for Coq
56Summary(pl.UTF-8): Tryb i składnia Coq dla Emacsa
57Group: Development/Tools
58Requires: %{name} = %{version}-%{release}
59
60%description emacs
61Emacs mode and suyntax files for Coq.
62
63%description emacs -l pl.UTF-8
64Pliki trybu i składni Coq dla Emacsa.
65
66%package latex
67Summary: Coq documentation style for latex
68Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa
69Group: Development/Tools
70Requires: %{name} = %{version}-%{release}
71
72%description latex
73Coq documentation style for latex.
74
75%description latex -l pl.UTF-8
76Styl dokumentacji Coq dla latexa.
77
680764bb
JR
78%prep
79%setup -q
5f0acdc3
JR
80%patch0 -p1
81
82%{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check
857e15b1 83%{__sed} -i -e 's|\(MAKE_TSOPTS=.*\) -s \(.*\)|\1 \2|' Makefile.build
680764bb
JR
84
85%build
86./configure \
87 -bindir %{_bindir} \
88 -libdir %{_libdir}/coq \
89 -mandir %{_mandir} \
2dc46485 90 -docdir %{_docdir}/%{name}-%{version} \
680764bb 91 -emacs emacs \
8f33d8d4 92 -browser "xdg-open %s" \
680764bb
JR
93 -emacslib %{_datadir}/emacs/site-lisp \
94 -opt \
1c74cbbc 95 --coqdocdir %{_datadir}/texmf/tex/latex/misc \
8bee228d 96 --coqide opt
680764bb 97
857e15b1
JR
98%{__make} -j1 world VERBOSE=1
99%{?with_tests:%{__make} -j1 check VERBOSE=1} # Use native coq to compile theories
680764bb
JR
100
101%install
102rm -rf $RPM_BUILD_ROOT
8bee228d 103install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}}
3432574d
JB
104
105%{__make} -e install \
106 COQINSTALLPREFIX=$RPM_BUILD_ROOT/
680764bb
JR
107# To install only locally the binaries compiled with absolute paths
108
8bee228d
JR
109install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir}
110install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir}
111
680764bb
JR
112%clean
113rm -rf $RPM_BUILD_ROOT
114
115%files
116%defattr(644,root,root,755)
861daf7b 117%attr(755,root,root) %{_bindir}/coq_makefile
9019ffc7 118%attr(755,root,root) %{_bindir}/coq-tex
680764bb 119%attr(755,root,root) %{_bindir}/coqc
2dc46485
JR
120%attr(755,root,root) %{_bindir}/coqchk
121%attr(755,root,root) %{_bindir}/coqchk.opt
680764bb 122%attr(755,root,root) %{_bindir}/coqdep
1c74cbbc 123%attr(755,root,root) %{_bindir}/coqdoc
5f0acdc3 124%attr(755,root,root) %{_bindir}/coqide*
861daf7b
JR
125%attr(755,root,root) %{_bindir}/coqmktop
126%attr(755,root,root) %{_bindir}/coqtop
127%attr(755,root,root) %{_bindir}/coqtop.byte
128%attr(755,root,root) %{_bindir}/coqtop.opt
1c74cbbc 129%attr(755,root,root) %{_bindir}/coqwc
861daf7b 130%attr(755,root,root) %{_bindir}/gallina
3432574d 131%dir %{_libdir}/coq
1c74cbbc 132%{_libdir}/coq/*
9019ffc7
JR
133%{_mandir}/man1/coq_makefile.1*
134%{_mandir}/man1/coq-tex.1*
680764bb 135%{_mandir}/man1/coqc.1*
2dc46485
JR
136%{_mandir}/man1/coqchk.1*
137%{_mandir}/man1/coqdep.1*
138%{_mandir}/man1/coqdoc.1*
2dc46485 139%{_mandir}/man1/coqide.1*
9019ffc7 140%{_mandir}/man1/coqmktop.1*
680764bb
JR
141%{_mandir}/man1/coqtop.1*
142%{_mandir}/man1/coqtop.byte.1*
143%{_mandir}/man1/coqtop.opt.1*
1c74cbbc 144%{_mandir}/man1/coqwc.1*
2dc46485 145%{_mandir}/man1/gallina.1*
8bee228d
JR
146%{_desktopdir}/coqide.desktop
147%{_pixmapsdir}/coqide.xpm
9019ffc7
JR
148
149%files emacs
150%defattr(644,root,root,755)
151%{_datadir}/emacs/site-lisp/coq.el
152%{_datadir}/emacs/site-lisp/coq-db.el
153%{_datadir}/emacs/site-lisp/coq-font-lock.el
154%{_datadir}/emacs/site-lisp/coq-inferior.el
155%{_datadir}/emacs/site-lisp/coq-syntax.el
156
157%files latex
158%defattr(644,root,root,755)
159%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
This page took 0.161817 seconds and 4 git commands to generate.