# 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.8
Release:	5%{?dist}
Summary:	Alt-Ergo automatic theorem prover

# Note: rpmlint invalid-license warning is incorrect - I had the
# CeCILL-C license reviewed by Fedora legal, and it is now present on
# http://fedoraproject.org/wiki/Licensing

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

%if 0%{?fedora} < 9
# There's no ocaml for ppc64 in Fedora <= 8
# bz# (will be changed when exists as a module):
ExcludeArch: ppc64
%endif

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

%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} swap0_why.why

%install
rm -rf %{buildroot}

mkdir -p %{buildroot}%{_bindir}
make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} 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
* 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.