File coq.spec of Package coq

#
# spec file for package ipe
#
# Copyright (c) 2009 SUSE LINUX Products GmbH, Nuernberg, Germany.
#
# All modifications and additions to the file contributed by third parties
# remain the property of their copyright owners, unless otherwise agreed
# upon. The license for this file, and modifications and additions to the
# file, is the same license as for the pristine package itself (unless the
# license for the pristine package is not an Open Source License, in which
# case the license is the MIT License). An “Open Source License” is a
# license that conforms to the Open Source Definition (Version 1.9)
# published by the Open Source Initiative.

# Please submit bugfixes or comments via http://bugs.opensuse.org/
#

# norootforbuild

%define main_ver 8.2
%define revision 1

Name:            coq
Version:         %{main_ver}.%{revision}
Release:         1
Summary:         The Coq Proof Assistant
License:         freely redistributable
Group:           Applications/Math
Vendor:          INRIA & LRI
URL:             http://coq.inria.fr
Source:          coq-%{main_ver}-%{revision}.tar.bz2
Source1:         coq.png
Source2:         coq.desktop
Icon:            petit-coq.gif
Requires:        ocaml-camlp5 >= 5.08 ncurses
BuildRoot:       %{_tmppath}/%{name}-%{version}-%{release}-buildroot

# Required for standard coq:
BuildRequires:   make >= 3.81 ocaml >= 3.10.0 ocaml-camlp5-devel >= 5.08 ncurses-devel
# For documentation:
BuildRequires:   LaTeX
# Required for coq-ide:
BuildRequires:   lablgtk2-devel >= 2.6 gtk2-devel >= 2.8 desktop-file-utils update-desktop-files

%description
Coq is a proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification.

This package contains shared files and the commandline interface. For GTK graphical interface install %{name}-ide.

%package ide
Summary:     IDE for The Coq Proof Assistant
Group:       Applications/Math
Requires:    gtk2 >= 2.8 lablgtk2 >= 2.6
Requires:    %{name} = %{version}-%{release}

%description ide
Coq is a proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification.

The Coq Integrated Development Interface is a graphical interface for the Coq proof assistant.

%package devel
Summary:     Development files for The Coq Proof Assistant
Group:       Development/Libraries/Other
Requires:    make >= 3.81 ocaml >= 3.10.0 camlp5-devel >= 5.08 ncurses-devel
Requires:    %{name} = %{version}-%{release}

%description devel
Coq is a proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification.

This package contains development files for Coq.

%prep
%setup -q -n %{name}-%{main_ver}-%{revision}

%build
export CFLAGS='%{optflags}'
./configure                \
   -bindir %{_bindir}      \
   -libdir %{_libdir}/coq  \
   -mandir %{_mandir}      \
   -emacslib %{_datadir}/emacs/site-lisp       \
   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
   -browser xdg-open \
   -fsets all        \
   -reals all        \
   -opt
make coq
make coqide

%clean
[ "%{buildroot}" != "/" ] && rm -rf %{buildroot}
make clean

%install
make COQINSTALLPREFIX=%{buildroot} install-coq
make COQINSTALLPREFIX=%{buildroot} install-coqide

install -D -m 644 %{SOURCE1} %{buildroot}%{_datadir}/icons/hicolor/128x128/apps/coq.png
%suse_update_desktop_file -i %SOURCE2
install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/applications/coq.desktop

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

%files ide
%defattr(-,root,root,-)
%{_bindir}/coqide*
%{_libdir}/coq/ide/*
%{_datadir}/icons/hicolor/128x128/apps/coq.png
%{_datadir}/applications/coq.desktop
%dir %{_libdir}/coq/ide

%files devel
%defattr(-,root,root,-)
%{_libdir}/coq/*.a
%{_libdir}/coq/*/*.a
%{_libdir}/coq/*/*.cmx
%{_libdir}/coq/*/*.cmxa

%changelog
* Wed Feb 25 2009 Radomir Cernoch <radomir.cernoch@gmail.com> - 8.2.1
- New version
- desktop-files added to Requires
* Thu Feb 20 2009 Radomir Cernoch <radomir.cernoch@gmail.com> - 8.2beta4
- Specfile cleaned up
- Development files moved to '-devel' package
* Mon Oct 20 2008 Radomir Cernoch <radomir.cernoch@gmail.com> - 8.2beta4
- Package created based on the original specfile provided by INRIA
- Coq and CoqIDE merged into one package as they have the same sources