- desktop file for coqide
[packages/coq.git] / coq.spec
CommitLineData
adfec888
JR
1#
2# TODO:
3# - desktop file for coqide
4#
521adcea 5Summary: The Coq Proof Assistant
374d5475 6Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu
680764bb 7Name: coq
72eff188 8Version: 8.3pl1
5f0acdc3 9Release: 1
680764bb
JR
10License: GPL
11Group: Applications/Math
12Vendor: INRIA Rocquencourt
5f0acdc3 13Source0: http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz
72eff188 14# Source0-md5: 1869d22b337f5da59ba3bbe1433f9a3b
5f0acdc3 15Patch0: %{name}-lablgtk2.patch
3432574d 16URL: http://coq.inria.fr/
5f0acdc3 17BuildRequires: bash
680764bb 18BuildRequires: emacs
861daf7b 19BuildRequires: ocaml >= 3.09.0
5f0acdc3 20BuildRequires: camlp5 >= 5.01
72eff188 21BuildRequires: ocaml-lablgtk2-devel >= 2.12.0
5f0acdc3 22BuildRequires: sed >= 4.0
680764bb
JR
23BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
24
25%description
26Coq is a proof assistant which:
bcd66107 27 - allows to handle calculus assertions,
28 - check mechanically proofs of these assertions,
29 - helps to find formal proofs,
30 - extracts a certified program from the constructive proof of its
31 formal specification.
3432574d 32
3f4e388b
JR
33%description -l pl.UTF-8
34Coq to narzędzie pomagające w udowadnianiu, które:
35- pozwala uporać się z twierdzeniami dotyczącymi rachunku
36 różniczkowego,
37- mechanicznie sprawdzać dowody tych twierdzeń,
38- pomagać w znalezieniu formalnych dowodów,
39- wyciągać program o dowiedzionej poprawności z konstruktywnego
bcd66107 40 dowodu jego formalnej specyfikacji.
680764bb
JR
41
42%prep
43%setup -q
5f0acdc3
JR
44%patch0 -p1
45
46%{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check
680764bb
JR
47
48%build
49./configure \
50 -bindir %{_bindir} \
51 -libdir %{_libdir}/coq \
52 -mandir %{_mandir} \
53 -emacs emacs \
54 -emacslib %{_datadir}/emacs/site-lisp \
55 -opt \
1c74cbbc 56 --coqdocdir %{_datadir}/texmf/tex/latex/misc \
861daf7b 57 --coqide opt \
1c74cbbc 58 -reals all # Need ocamlc.opt and ocamlopt.opt
680764bb 59
5f0acdc3 60%{__make} -j1 world check # Use native coq to compile theories
680764bb
JR
61
62%install
63rm -rf $RPM_BUILD_ROOT
3432574d
JB
64
65%{__make} -e install \
66 COQINSTALLPREFIX=$RPM_BUILD_ROOT/
680764bb
JR
67# To install only locally the binaries compiled with absolute paths
68
69%clean
70rm -rf $RPM_BUILD_ROOT
71
72%files
73%defattr(644,root,root,755)
861daf7b
JR
74%attr(755,root,root) %{_bindir}/coq-interface
75%attr(755,root,root) %{_bindir}/coq-interface.opt
76%attr(755,root,root) %{_bindir}/coq-tex
77%attr(755,root,root) %{_bindir}/coq_makefile
680764bb 78%attr(755,root,root) %{_bindir}/coqc
680764bb 79%attr(755,root,root) %{_bindir}/coqdep
1c74cbbc 80%attr(755,root,root) %{_bindir}/coqdoc
5f0acdc3 81%attr(755,root,root) %{_bindir}/coqide*
861daf7b
JR
82%attr(755,root,root) %{_bindir}/coqmktop
83%attr(755,root,root) %{_bindir}/coqtop
84%attr(755,root,root) %{_bindir}/coqtop.byte
85%attr(755,root,root) %{_bindir}/coqtop.opt
1c74cbbc 86%attr(755,root,root) %{_bindir}/coqwc
861daf7b 87%attr(755,root,root) %{_bindir}/gallina
680764bb 88%attr(755,root,root) %{_bindir}/parser
1c74cbbc 89%attr(755,root,root) %{_bindir}/parser.opt
3432574d 90%dir %{_libdir}/coq
1c74cbbc 91%{_libdir}/coq/*
680764bb
JR
92%{_datadir}/emacs/site-lisp/coq.el
93%{_datadir}/emacs/site-lisp/coq-inferior.el
94%{_mandir}/man1/coq-tex.1*
95%{_mandir}/man1/coqdep.1*
96%{_mandir}/man1/gallina.1*
97%{_mandir}/man1/coqc.1*
98%{_mandir}/man1/coqtop.1*
99%{_mandir}/man1/coqtop.byte.1*
100%{_mandir}/man1/coqtop.opt.1*
101%{_mandir}/man1/coq_makefile.1*
102%{_mandir}/man1/coqmktop.1*
103%{_mandir}/man1/coq-interface.1*
104%{_mandir}/man1/parser.1*
1c74cbbc 105%{_mandir}/man1/coqdoc.1*
106%{_mandir}/man1/coqwc.1*
107%{_datadir}/texmf/tex/latex/misc/coqdoc.sty
This page took 0.041647 seconds and 4 git commands to generate.