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