# 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.94
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
Source3:	%{name}.desktop

BuildRequires:	desktop-file-utils
BuildRequires:	gtksourceview2-devel
BuildRequires:	ocaml
BuildRequires:	ocaml-lablgtk-devel
BuildRequires:	ocaml-ocamlgraph-devel
BuildRequires:	prelink

Requires(post):	coreutils

ExclusiveArch:	%{ocaml_arches}

# Filter out symbols that are provided by interface files (*.mli) only.
# There are no corresponding symbols available at runtime.
%global __requires_exclude ocaml\\\(((Sig)|(Smt_ast)|(Why_ptree))\\\)

%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}
Requires:	gtksourceview2

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

%prep
%setup -q

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

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

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

# Remove files we do not want installed
rm -f %{buildroot}%{_datadir}/%{name}/*.{cmx,o}

# 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

# Install the gtksourceview2 support
mkdir -p %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs
cp -p util/gtk-lang/alt-ergo.lang \
      %{buildroot}%{_datadir}/gtksourceview-2.0/language-specs

# Install the desktop file
mkdir -p %{buildroot}%{_datadir}/applications
desktop-file-install --dir %{buildroot}%{_datadir}/applications %{name}.desktop

%post gui
update-desktop-database &> /dev/null || :

%postun gui
update-desktop-database &> /dev/null || :

# 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

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

%files gui
%{_bindir}/altgr-ergo
%{_datadir}/applications/%{name}.desktop
%{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang

%changelog
* Tue Dec  6 2011 Jerry James <loganjerry@gmail.com> - 0.94-1
- Add a desktop file for the gui.
- Update to version 0.94.  This means:
- The theory of records replaces the theory of pairs
- Bug fixes (intervals, term data-structure, stack-overflows, matching,
  existentials, distincts, CC, GUI)
- Improvements (SMT-Lib2 front-end, intervals, case-splits, triggers, lets)
- Multiset ordering for AC(X)
- Manual lemma instantiation in the GUI

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