[packages/coq.git] / coq.spec

Summary:	The Coq Proof Assistant
Summary(pl.UTF-8):	Coq - narzędzie pomagające w udowadnianiu
Name:		coq
Version:	8.1pl4
Release:	1
License:	GPL
Group:		Applications/Math
Vendor:		INRIA Rocquencourt
Source0:	http://coq.inria.fr/V%{version}/files/%{name}-%{version}.tar.gz
# Source0-md5:	8fa623538d362d8f48d78e598c43215e
Patch0:		%{name}-lablgtk2.patch
URL:		http://coq.inria.fr/
BuildRequires:	bash
BuildRequires:	emacs
BuildRequires:	ocaml >= 3.09.0
BuildRequires:	camlp5 >= 5.01
BuildRequires:	ocaml-lablgtk2-devel >= 2.6.0
BuildRequires:	sed >= 4.0
BuildRoot:	%{tmpdir}/%{name}-%{version}-root-%(id -u -n)

%description
Coq is a proof assistant which:
 - allows to handle calculus assertions,
 - check mechanically proofs of these assertions,
 - helps to find formal proofs,
 - extracts a certified program from the constructive proof of its
   formal specification.

%description -l pl.UTF-8
Coq to narzędzie pomagające w udowadnianiu, które:
- pozwala uporać się z twierdzeniami dotyczącymi rachunku
  różniczkowego,
- mechanicznie sprawdzać dowody tych twierdzeń,
- pomagać w znalezieniu formalnych dowodów,
- wyciągać program o dowiedzionej poprawności z konstruktywnego
  dowodu jego formalnej specyfikacji.

%prep
%setup -q
%patch0 -p1

%{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check

%build
./configure \
	-bindir %{_bindir} \
	-libdir %{_libdir}/coq \
	-mandir %{_mandir} \
	-emacs emacs \
	-emacslib %{_datadir}/emacs/site-lisp \
	-opt \
	--coqdocdir %{_datadir}/texmf/tex/latex/misc \
	--coqide opt \
	-reals all	# Need ocamlc.opt and ocamlopt.opt 

%{__make} -j1 world check	# Use native coq to compile theories

%install
rm -rf $RPM_BUILD_ROOT

%{__make} -e install \
	COQINSTALLPREFIX=$RPM_BUILD_ROOT/
# To install only locally the binaries compiled with absolute paths

%clean
rm -rf $RPM_BUILD_ROOT

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