# Exclude a private ocaml interface that we don't Provide, and a Provides that
# the automatic generator is failing to produce for ocaml-lablgtk
%global __requires_exclude ocaml\\\((Interface|GtkSourceView2_types)\\\)
Name: coq
Version: 8.5pl2
Release: %mkrel 2
Summary: The Coq Proof Assistant
Group: Sciences/Computer science
License: LGPLv2
URL: https://coq.inria.fr
Source0: https://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz
Source1: https://coq.inria.fr/distrib/V%{version}/files/Tutorial.pdf
Source2: https://coq.inria.fr/distrib/V%{version}/files/Reference-Manual.pdf
Source3: https://coq.inria.fr/distrib/V%{version}/files/RecTutorial.pdf
BuildRequires: ocaml-compiler
BuildRequires: ocaml-compiler-libs
BuildRequires: camlp5
BuildRequires: ocaml-lablgtk2-devel
BuildRequires: ncurses-devel
BuildRequires: texlive
BuildRequires: imagemagick
%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} \
%{SOURCE3} .
%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}/%{name} \
-browser "xdg-open %s" \
-usecamlp5 \
-lablgtkdir %{_libdir}/ocaml/lablgtk2 \
-opt -debug
export CAML_LD_LIBRARY_PATH=$PWD/kernel/byterun:${CAML_LD_LIBRARY_PATH}
make world
%install
make COQINSTALLPREFIX=%{buildroot} install-coq
make COQINSTALLPREFIX=%{buildroot} install-coqide
export EXCLUDE_FROM_STRIP=%{_bindir}
for png in 256x256 48x48 32x32 16x16; do
mkdir -p %{buildroot}%{_iconsdir}/hicolor/${png}/apps/
convert -geometry $png ide/%{name}.png %{buildroot}%{_iconsdir}/hicolor/${png}/apps/%{name}.png
done
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 COMPATIBILITY README CREDITS
%license COPYRIGHT LICENSE
%doc %{_docdir}/%{name}/FAQ-CoqIde
%{_bindir}/*
%{_libdir}/coq
%{_mandir}/man1/*
%{_datadir}/emacs/site-lisp/*
%{_datadir}/texmf/tex/latex/misc/*
%{_datadir}/%{name}/
%exclude %{_bindir}/coqide*
%exclude %{_libdir}/coq/ide
%files ide
%doc ide/FAQ
%{_sysconfdir}/xdg/coq/
%{_datadir}/applications/%{name}.desktop
%{_iconsdir}/hicolor/*/apps/%{name}.png
%{_bindir}/coqide*
%{_libdir}/coq/ide
%files doc
%doc Tutorial.pdf
%doc Reference-Manual.pdf
%doc RecTutorial.pdf
%changelog
* Sun Sep 25 2016 pterjan <pterjan> 8.5pl2-2.mga6
+ Revision: 1056205
- Rebuild for fix in ocaml
* Sun Sep 18 2016 daviddavid <daviddavid> 8.5pl2-1.mga6
+ Revision: 1053630
- new version: 8.5pl2
- update URL and Sources URL
- exclude a private ocaml interface that we don't Provide, and a Provides that
the automatic generator is failing to produce for ocaml-lablgtk
- add RecTutorial.pdf as a doc file
- update doc files and files list
* Tue Feb 02 2016 pterjan <pterjan> 8.4pl6-1.mga6
+ Revision: 930946
- Update to 8.4pl6
* Fri Sep 11 2015 neoclust <neoclust> 8.4pl4-7.mga6
+ Revision: 876969
- Enable debug
* Fri Sep 11 2015 neoclust <neoclust> 8.4pl4-6.mga6
+ Revision: 876939
- Fix build with new rpm ( empty debuginfo)
* Wed Oct 15 2014 umeabot <umeabot> 8.4pl4-5.mga5
+ Revision: 740302
- Second Mageia 5 Mass Rebuild
* Fri Sep 26 2014 tv <tv> 8.4pl4-4.mga5
+ Revision: 725007
- rebuild for bogus file deps
* Thu Sep 18 2014 umeabot <umeabot> 8.4pl4-3.mga5
+ Revision: 693686
- Rebuild to fix library dependencies
* Tue Sep 16 2014 umeabot <umeabot> 8.4pl4-2.mga5
+ Revision: 678542
- Mageia 5 Mass Rebuild
* Mon Jun 23 2014 malo <malo> 8.4pl4-1.mga5
+ Revision: 638780
- update to 8.4pl4
* Sat Oct 19 2013 umeabot <umeabot> 8.4pl2-3.mga4
+ Revision: 527415
- Mageia 4 Mass Rebuild
+ luigiwalser <luigiwalser>
- fix check for make version
* Fri Jun 07 2013 malo <malo> 8.4pl2-1.mga4
+ Revision: 440012
- update to 8.4pl2 (patch from William Murphy)
* 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
