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