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