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