# 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.

# The following are necessary for alt-ergo to depend on the correct
# version of ocaml-ocamlgraph

%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%define debug_package %{nil}
%define _use_internal_dependency_generator 0
%define __find_requires /usr/lib/rpm/ocaml-find-requires.sh
%define __find_provides /usr/lib/rpm/ocaml-find-provides.sh

Name:		alt-ergo
Version:	0.92.1
Release:	1%{?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
BuildRoot:	%{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)

BuildRequires:	ocaml, ocaml-ocamlgraph-devel, prelink

# Still no ocaml on s390(x) or sparc64
ExcludeArch: s390 s390x sparc64

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

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

mv CeCILL-C CeCILL-C.iso8859
iconv -f ISO-8859-1 -t UTF-8 < CeCILL-C.iso8859 > CeCILL-C
rm CeCILL-C.iso8859

%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
rm -rf %{buildroot}

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

%clean
rm -rf %{buildroot}

%files
%defattr(-,root,root,-)
%{_bindir}/*
%{_datadir}/%{name}
%{_mandir}/man1/alt-ergo.1.gz
%doc README.alt-ergo COPYING CeCILL-C CHANGES

%changelog
* 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.