Name:		coq
Version:	8.3pl3
Release:	%mkrel 1
Summary:	The Coq Proof Assistant
Group:		Sciences/Computer science
License:	LGPL
URL:		http://coq.inria.fr
Source:		http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz
BuildRequires:	ocaml
BuildRequires:	camlp5
BuildRequires:	ocaml-lablgtk2-devel
BuildRequires:	ncurses-devel
BuildRequires:	hevea
BuildRequires:	tetex-latex

%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} \
            -browser "xdg-open %s" \
            -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
* Thu Feb 09 2012 Andrey Bondrov <abondrov@mandriva.org> 8.3pl3-1mdv2012.0
+ Revision: 772236
- Update BuildRequires (add tetex-latex)
- New version 8.3pl3, update BuildRequires and build options

* Mon Jul 18 2011 Guillaume Rousse <guillomovitch@mandriva.org> 8.3pl2-1
+ Revision: 690589
- new version

* Mon Dec 20 2010 Guillaume Rousse <guillomovitch@mandriva.org> 8.3-3mdv2011.0
+ Revision: 623284
- new version

  + Oden Eriksson <oeriksson@mandriva.com>
    - rebuild

* 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 <tv@mandriva.org>
    - rebuild
    - kill re-definition of %%buildroot on Pixel's request

  + Olivier Blin <blino@mandriva.org>
    - 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