# rpmlint "no-binary" error is not really an error - see:
# https://www.redhat.com/archives/fedora-packaging/2008-August/msg00017.html
# and ocaml-ocamlgraph spec file for a discussion of this issue.

%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%define debug_package %{nil}

Name:		alt-ergo
Version:	0.93
Release:	2%{?dist}
Summary:	Automated theorem prover including linear arithmetic

Group:		Applications/Engineering
License:	CeCILL-C
URL:		http://alt-ergo.lri.fr/
Source0:	http://alt-ergo.lri.fr/http/alt-ergo-%{version}.tar.gz
Source1:	swap0_why.why
Source2:	README.alt-ergo

BuildRequires:	gtksourceview2-devel
BuildRequires:	ocaml
BuildRequires:	ocaml-lablgtk-devel
BuildRequires:	ocaml-ocamlgraph-devel
BuildRequires:	prelink

Requires(post): coreutils

ExclusiveArch:  %{ocaml_arches}

%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:		Applications/Engineering
Requires:	%{name}%{?_isa} = %{version}-%{release}

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

%prep
%setup -q

cp -p %{SOURCE1} %{SOURCE2} .

# Set print_flag to false or invoking with -select
# from "why" will pause every invocation :-(.
sed -i -e 's/let print_flag = true/let print_flag = false/;' pruning.ml

%build
# Avoid a Makefile patch by just adding this empty file, and thus autoconf
# doesn't complain (better than ignoring all status from configure)
touch version.sh.in
./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir}

%if ! %{opt}
%define opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex
%else
%define opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif

make %{opt_option}
make %{opt_option} gui

iconv -f ISO-8859-1 -t UTF-8 -o CeCILL-C.utf8 CeCILL-C
touch -r CeCILL-C CeCILL-C.utf8
mv -f CeCILL-C.utf8 CeCILL-C

%if %{opt}
strip ./alt-ergo.opt
execstack -c ./alt-ergo.opt
%endif

# Test alt-ergo on fairly trivial why file - generated from why example swap0.mlw w/why v2.14
%check
%if %opt
%define altergo ./alt-ergo.opt
%else
%define altergo ./alt-ergo.byte
%endif
%{altergo} -arrays swap0_why.why

%install
mkdir -p %{buildroot}%{_bindir}
make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir}/%{name} MANDIR=%{buildroot}%{_mandir} install

# Have to install the GUI by hand due to hardcoded paths in the makefile
%if %opt
strip altgr-ergo.opt
cp -p altgr-ergo.opt %{buildroot}%{_bindir}/altgr-ergo
%else
cp -p altgr-ergo.byte %{buildroot}%{_bindir}/altgr-ergo
%endif
cp -p util/gtk-lang/alt-ergo.lang %{buildroot}%{_datadir}/%{name}

%post gui
if [ -d %{_datadir}/gtksourceview-2.0/language-specs ]; then
  cp -p %{_datadir}/%{name}/alt-ergo.lang \
	%{_datadir}/gtksourceview-2.0/language-specs
fi

%triggerun gui -- gtksourceview2
rm -f %{_datadir}/gtksourceview-2.0/language-specs/alt-ergo.lang

%files
%{_bindir}/%{name}
%dir %{_datadir}/%{name}
%{_datadir}/%{name}/smt_prelude.mlw
%{_mandir}/man1/alt-ergo.1.*
%doc README.alt-ergo COPYING CeCILL-C CHANGES

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

%changelog
* Mon Nov 14 2011 Jerry James <loganjerry@gmail.com> - 0.93-2
- Build on all arches with ocaml

* Thu May 12 2011 Jerry James <loganjerry@gmail.com> - 0.93-1
- Update to version 0.93.  This means:
- New command-line options -steps, -max-split, and -proof
- New polymorphic theory of arrays
- Built-in support for enumeration types
- Graphical front end
- New predicate distinct()
- New constructs: let x = <term> in <term>, let x = <term> in <formula>
- Partial support for the division operator
- Unspecified bug fixes

* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.92.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild

* Tue Oct 06 2010 David A. Wheeler <dwheeler@dwheeler.com> 0.92.1-1
- Update to version 0.92.1. This means:
- New built-in syntax for the theory of arrays
- Fixes a bug in the arithmetic module
- Allows folding and unfolding of predicate definitions

* Tue Jun 08 2010 David A. Wheeler <dwheeler@dwheeler.com> 0.91-1
- Update to version 0.91. This means:
- partial support for non-linear arithmetics
- support case split on integer variables
- new support for Euclidean division and modulo operators


* Tue Aug 04 2009 Alan Dunn <amdunn@gmail.com> 0.9-2
- Added ExcludeArch sparc64 due to no OCaml

* Fri Jul 24 2009 Alan Dunn <amdunn@gmail.com> 0.9-1
- New upstream version
- Removed code for check for Fedora version (8) that is EOL
- Removed comments re: CeCILL-C license as it is ok to have (no
  rpmlint warnings to explain either).

* Wed Jun 17 2009 Karsten Hopp <karsten@redhat.com> 0.8-5.1
- ExcludeArch s390x as there's no ocaml available

* Mon Feb 23 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.8-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild

* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 0.8-4
- Rebuild: Source upstream appears to have changed even with same version number
  (seems like bug fix from examination of changes)
- Changed hardcoded version number in source string
* Fri Sep 05 2008 Alan Dunn <amdunn@gmail.com> 0.8-3
- Fixed BuildRequires to add prelink (for execstack).
* Tue Aug 26 2008 Alan Dunn <amdunn@gmail.com> 0.8-2
- Fixed BuildRequires to add ocaml-ocamlgraph-devel instead of
  ocaml-ocamlgraph, made other minor changes.
* Mon Aug 25 2008 Alan Dunn <amdunn@gmail.com> 0.8-1
- Initial Fedora RPM version.