%define name    alt-ergo
%define version 0.94
%define release %mkrel 3

Summary: Automated theorem prover including linear arithmetic
Name:    %{name}
Version: %{version}
Release: %{release}
Source0: http://alt-ergo.lri.fr/http/%{name}-%{version}.tar.gz
License: CeCILL-C
Group:   Sciences/Computer science
Url:     http://alt-ergo.lri.fr

BuildRequires:  gtksourceview2-devel
BuildRequires:  ocaml-compiler
BuildRequires:  ocaml-lablgtk2-devel
BuildRequires:  ocaml-ocamlgraph-devel

%description
Alt-Ergo is an automated theorem prover implemented in OCaml. It is
based on CC(X) - a congruence closure algorithm parameterized by an
equational theory X. This algorithm is reminiscent of the Shostak
algorithm. Currently CC(X) is instantiated by the theory of linear
arithmetics. Alt-Ergo also contains a home made SAT-solver and an
instantiation mechanism by which it fully supports quantifiers.

%package gui
Summary:  Graphical front end for alt-ergo
Group:    Sciences/Computer science
Requires: %{name} = %{version}
Requires: gtksourceview2

%description gui
A graphical front end for the alt-ergo theorem prover.


%prep
%setup -q

%build
./configure \
        --prefix=%{_prefix} \
        --bindir=%{_bindir} \
        --libdir=%{_datadir} \
        --mandir=%{_mandir}
make opt gui


%install
rm -rf %{buildroot}
make BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_libdir}/ocaml/%{name} MANDIR=%{buildroot}%{_mandir} install

# Installing gui by hand
cp -p altgr-ergo.opt %{buildroot}%{_bindir}/altgr-ergo
mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
mkdir -p %{buildroot}%{_datadir}/%{name}
cp -p util/gtk-lang/alt-ergo.lang %{buildroot}%{_datadir}/%{name}/
cp -p util/gtk-lang/alt-ergo.lang %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs/

# Removing un-needed files
rm -f %{buildroot}%{_libdir}/ocaml/%{name}/*.{cmx,o}

%files
%{_bindir}/%{name}
%dir %{_libdir}/ocaml/%{name}
%{_libdir}/ocaml/%{name}/altErgo.cmi
%{_libdir}/ocaml/%{name}/altErgo.cmo
%{_mandir}/man1/alt-ergo.1.*
%doc README CeCILL-C CHANGES


%files gui
%{_bindir}/altgr-ergo
%dir %{_datadir}/%{name}
%{_datadir}/%{name}/alt-ergo.lang
%attr(644,-,-) %{_datadir}/gtksourceview-2.0/language-specs/alt-ergo.lang


%changelog

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

* Tue Dec 04 2012 malo <malo> 0.94-2.mga3
+ Revision: 326565
+ rebuild (emptylog)

* Tue Dec 04 2012 malo <malo> 0.94-1.mga3
+ Revision: 326543
- change BR to ocaml-compiler

* Sun Dec 11 2011 malo <malo> 0.94-1.mga2
+ Revision: 180489
- new version 0.94
- missing Requires gtksourceview2
- fixing install of source.lang and ocaml lib

* Sat Nov 05 2011 malo <malo> 0.93-1.mga2
+ Revision: 163891
- imported package alt-ergo