%define name	coq
%define version	8.2pl1
%define release	%mkrel 2

Name:		%{name}
Version:	%{version}
Release:	%{release}
Summary:	The Coq Proof Assistant
Group:		Sciences/Computer science
License:	LGPL
URL:		http://coq.inria.fr
Source:		ftp://ftp.inria.fr/INRIA/coq/V%{version}/%{name}-%{version}.tar.gz
BuildRequires:	ocaml >= 3.06
BuildRequires:	camlp5
BuildRequires:	ocaml-lablgtk2-devel
BuildRequires:	ncurses-devel
Buildroot:	%{_tmppath}/%{name}-%{version}

%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, 

%package ide
Summary:	The Coq Integrated Development Interface
Group:		Sciences/Computer science
Requires:	%{name} = %{version}

%description ide
The Coq Integrated Development Interface is a graphical interface for the 
Coq proof assistant 

%prep
%setup -q

%build
./configure --mandir %{_mandir} \
            --bindir %{_bindir} \
            --libdir %{_libdir}/coq \
            --emacslib %{_datadir}/emacs/site-lisp \
            --coqdocdir %{_datadir}/texmf/tex/latex/misc \
            --docdir %{_datadir}/doc/%{name} \
            --reals all \
            --opt
make world

%clean
rm -rf %{buildroot}

%install
rm -rf %{buildroot}
make COQINSTALLPREFIX=%{buildroot} install-coq
make COQINSTALLPREFIX=%{buildroot} install-coqide
export EXCLUDE_FROM_STRIP=%{_bindir}

%files
%defattr(-,root,root)
%doc CHANGES COPYRIGHT README CREDITS INSTALL LICENSE
%{_bindir}/*
%{_libdir}/coq
%{_mandir}/man1/*
%{_datadir}/emacs/site-lisp/*
%{_datadir}/texmf/tex/latex/misc/*
%exclude %{_bindir}/coqide*
%exclude %{_libdir}/coq/ide

%files ide
%doc INSTALL.ide
%defattr(-,root,root)
%{_bindir}/coqide*
%{_libdir}/coq/ide


%changelog
* Wed Feb 10 2010 Guillaume Rousse <guillomovitch@mandriva.org> 8.2pl1-2mdv2010.1
+ Revision: 503738
- rebuild
- new version

* Mon Jun 29 2009 Guillaume Rousse <guillomovitch@mandriva.org> 8.2-2mdv2010.0
+ Revision: 390561
- rebuild for latest ocaml

* Wed Feb 18 2009 Guillaume Rousse <guillomovitch@mandriva.org> 8.2-1mdv2009.1
+ Revision: 342724
- final 8.2 version

* Sun Feb 15 2009 Guillaume Rousse <guillomovitch@mandriva.org> 8.2-0.rc2.1mdv2009.1
+ Revision: 340578
- new release

* Sun Aug 17 2008 Guillaume Rousse <guillomovitch@mandriva.org> 8.1pl3-1mdv2009.0
+ Revision: 272986
- new version

  + Thierry Vignaud <tvignaud@mandriva.com>
    - rebuild
    - kill re-definition of %%buildroot on Pixel's request

  + Olivier Blin <oblin@mandriva.com>
    - restore BuildRoot

* Fri Sep 28 2007 Guillaume Rousse <guillomovitch@mandriva.org> 8.1pl1-1mdv2008.0
+ Revision: 93431
- new version

  + Pascal Terjan <pterjan@mandriva.org>
    - Rebuild to sync with x86_64
    - Import coq



* Tue Aug 29 2006 Guillaume Rousse <guillomovitch@mandriva.org> 8.0pl3-5mdv2007.0
- Rebuild

* Mon Mar 27 2006 Guillaume Rousse <guillomovitch@mandriva.org> 8.0pl3-4mdk
- buildrequires

* Fri Mar 17 2006 Guillaume Rousse <guillomovitch@mandriva.org> 8.0pl3-3mdk
- disable stripping, as it breaks binaries

* Wed Mar 15 2006 Guillaume Rousse <guillomovitch@mandriva.org> 8.0pl3-2mdk
- add patch for ocaml 3.0.9
- buildrequires

* Thu Mar 02 2006 Guillaume Rousse <guillomovitch@mandriva.org> 8.0pl3-1mdk
- first mdk release