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

BuildRequires:  gtksourceview2-devel
BuildRequires:  ocaml-compiler
BuildRequires:  ocaml-lablgtk2-devel
BuildRequires:  ocaml-ocamlgraph-devel
BuildRequires:  ocaml-zarith-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=%{_libdir} \
        --datadir=%{_datadir} \
        --mandir=%{_mandir}
make opt gui


%install
make BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_libdir}/ocaml/%{name} MANDIR=%{buildroot}%{_mandir} DATADIR=%{buildroot}%{_datadir} install install-gui

mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs/
cp doc/gtk-lang/alt-ergo.lang %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs/

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

%files
%{_bindir}/%{name}
%{_mandir}/man1/alt-ergo.1.*
%doc README.md LICENSE CHANGES doc/


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


%changelog
* Wed Oct 15 2014 umeabot <umeabot> 0.95.2-4.mga5
+ Revision: 743440
- Second Mageia 5 Mass Rebuild

* Tue Sep 16 2014 umeabot <umeabot> 0.95.2-3.mga5
+ Revision: 677745
- Mageia 5 Mass Rebuild

* Tue Oct 22 2013 umeabot <umeabot> 0.95.2-2.mga4
+ Revision: 543622
- Mageia 4 Mass Rebuild

* Tue Oct 15 2013 malo <malo> 0.95.2-1.mga4
+ Revision: 498662
- new version 0.95.2

* Fri May 31 2013 malo <malo> 0.95.1-1.mga4
+ Revision: 433869
- new version 0.95.1

* 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