Name:           coq
Version:        8.4pl1
Release:        %mkrel 1
Summary:        The Coq Proof Assistant
Group:          Sciences/Computer science
License:        LGPLv2
URL:            http://coq.inria.fr
Source0:        http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz
Source1:        http://coq.inria.fr/distrib/V8.4/files/Tutorial.pdf
Source2:        http://coq.inria.fr/distrib/V8.4/files/Reference-Manual.pdf
BuildRequires:  ocaml-compiler
BuildRequires:  ocaml-compiler-libs
BuildRequires:  camlp5
BuildRequires:  ocaml-lablgtk2-devel
BuildRequires:  ncurses-devel
BuildRequires:  texlive

%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 


%package doc
Summary:        Documentation for %{name}
Group:          Documentation
License:        Open Publication License
BuildArch:      noarch

%description doc
The %{name}-doc package contains documentation for %{name}.

%prep
%setup -q

cp %{SOURCE1} \
   %{SOURCE2} .

%build
./configure \
        -mandir %{_mandir} \
        -bindir %{_bindir} \
        -libdir %{_libdir}/coq \
        -emacslib %{_datadir}/emacs/site-lisp \
        -coqdocdir %{_datadir}/texmf/tex/latex/misc \
        -configdir %{_sysconfdir}/xdg/coq \
        -docdir %{_datadir}/doc/%{name} \
        -datadir %{_datadir}/pixmaps \
        -browser "xdg-open %s" \
        -usecamlp5 \
        -lablgtkdir %{_libdir}/ocaml/lablgtk2 \
        -opt
export CAML_LD_LIBRARY_PATH=`pwd`/kernel/byterun:${CAML_LD_LIBRARY_PATH}
make world


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

mkdir -p %{buildroot}%{_datadir}/applications
cat > %{buildroot}%{_datadir}/applications/%{name}.desktop << EOF
[Desktop Entry]
Name=CoqIDE
Comment=Coq integrated developpment environment
Exec=%{_bindir}/coqide
Icon=coq
Type=Application
Categories=Education;Science;Math;
EOF


%files
%doc CHANGES COPYRIGHT README CREDITS INSTALL LICENSE
%{_bindir}/*
%{_libdir}/coq
%{_mandir}/man1/*
%{_datadir}/emacs/site-lisp/*
%{_datadir}/texmf/tex/latex/misc/*
%{_datadir}/pixmaps/coq.png
%exclude %{_bindir}/coqide*
%exclude %{_libdir}/coq/ide

%files ide
%doc INSTALL.ide
%{_sysconfdir}/xdg/coq/coqide-gtk2rc
%{_datadir}/applications/%{name}.desktop
%{_bindir}/coqide*
%{_libdir}/coq/ide

%files doc
%doc Tutorial.pdf
%doc Reference-Manual.pdf


%changelog

* Mon Jan 14 2013 malo <malo> 8.4pl1-1.mga3
+ Revision: 387353
- new bugfix release 8.4pl1
- remove patch which was included upstream

* Fri Jan 11 2013 umeabot <umeabot> 8.4-3.mga3
+ Revision: 348157
- Mass Rebuild - https://wiki.mageia.org/en/Feature:Mageia3MassRebuild

* Tue Oct 02 2012 blue_prawn <blue_prawn> 8.4-2.mga3
+ Revision: 302076
- build requires ocaml-compiler-libs
- rebuild with new ocaml 4.00
- also include documentation

* Sun Aug 26 2012 malo <malo> 8.4-1.mga3
+ Revision: 284166
- missing buildrequires on camlp4-devel
- update to version 8.4
- add patch from Gentoo for compatibility with lablgtk 2.16
- add desktop file for the IDE

* Sun Jul 29 2012 malo <malo> 8.3pl4-1.mga3
+ Revision: 275566
- new version 8.3pl4
- fix requires to ocaml-compiler

* Sat Jan 14 2012 malo <malo> 8.3pl3-1.mga2
+ Revision: 195965
- new version 8.3pl3

* Sun Oct 23 2011 malo <malo> 8.3pl2-1.mga2
+ Revision: 157538
- imported package coq


* Mon Jul 18 2011 Guillaume Rousse <guillomovitch@mandriva.org> 8.3pl2-1mdv2012.0
+ 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 <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