%global __requires_exclude ^ocaml\\(Matching_types|NumbersInterface\\).*$

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

BuildRequires:  pkgconfig(gtksourceview-2.0)
BuildRequires:  ocaml-menhir
BuildRequires:  ocaml-compiler
BuildRequires:  ocaml-camlzip-devel
BuildRequires:  ocaml-findlib-devel
BuildRequires:  ocaml-lablgtk2-devel
BuildRequires:  ocaml-num-devel
BuildRequires:  ocaml-ocamlgraph-devel
BuildRequires:  ocaml-ocplib-simplex-devel
BuildRequires:  ocaml-zarith-devel
BuildRequires:  ocaml-psmt2-frontend

%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
%autosetup

%build
%configure2_5x
%__make opt gui

%install
%make_install install-gui

# Move the gtksourceview file to the right place
mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir}

# 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.*
%{_libdir}/alt-ergo/
%doc README.md LICENSE.md CHANGES doc/


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


%changelog
* Thu Oct 25 2018 daviddavid <daviddavid> 2.2.0-5.mga7
+ Revision: 1325199
- rebuild for new ocaml 4.07.1

* Fri Sep 21 2018 umeabot <umeabot> 2.2.0-4.mga7
+ Revision: 1294308
- Mageia 7 Mass Rebuild

* Tue May 08 2018 kekepower <kekepower> 2.2.0-3.mga7
+ Revision: 1227647
- Fix the global exclude

* Tue May 08 2018 kekepower <kekepower> 2.2.0-2.mga7
+ Revision: 1227641
- Exclude bogus requires

* Sun Apr 29 2018 kekepower <kekepower> 2.2.0-1.mga7
+ Revision: 1223246
- BR ocaml-psmt2-frontend
- Update to version 2.2.0

* Sun Mar 25 2018 daviddavid <daviddavid> 2.1.0-3.mga7
+ Revision: 1212412
- rebuild for new ocaml-zarith 1.7

* Fri Mar 23 2018 kekepower <kekepower> 2.1.0-2.mga7
+ Revision: 1211584
- Rebuild on arm

* Fri Mar 23 2018 kekepower <kekepower> 2.1.0-1.mga7
+ Revision: 1211568
- Add LGPL license
- Fix file list
- Add BR for menhir
- Update to version 2.1.0

* Tue Feb 06 2018 daviddavid <daviddavid> 1.30-2.mga7
+ Revision: 1199171
- add BR ocaml-num-devel

* Sat Jan 21 2017 daviddavid <daviddavid> 1.30-1.mga6
+ Revision: 1082661
- new version: 1.30
- add BRs ocaml-camlzip-devel and ocaml-camlzip-devel

* Sun Sep 25 2016 pterjan <pterjan> 1.01-2.mga6
+ Revision: 1056198
- Rebuild for fix in ocaml

* Sat Mar 26 2016 daviddavid <daviddavid> 1.01-1.mga6
+ Revision: 995605
- new version: 1.01

* Mon Jan 25 2016 daviddavid <daviddavid> 0.99.1-1.mga6
+ Revision: 927350
- new version: 0.99.1

* 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