[alt-ergo] Update to version 0.93.

[Jerry James]

commit fd511439b8e1649466fdd7e531a96f8c7de77879
Author: Jerry James <loganjerry at gmail.com>
Date:   Thu May 12 20:27:13 2011 -0600

    Update to version 0.93.

 .gitignore    |    4 +--
 alt-ergo.spec |   84 ++++++++++++++++++++++++++++++++++++++++----------------
 sources       |    2 +-
 3 files changed, 62 insertions(+), 28 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index dbaa9e8..dd524f0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1 @@
-alt-ergo-0.9.tar.gz
-alt-ergo-0.91.tar.gz
-/alt-ergo-0.92.1.tar.gz
+/alt-ergo-0.93.tar.gz
diff --git a/alt-ergo.spec b/alt-ergo.spec
index 9d06e40..44f44d5 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -2,18 +2,12 @@
 # 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:	2%{?dist}
+Version:	0.93
+Release:	1%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 Group:		Applications/Engineering
@@ -22,15 +16,19 @@ 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
+BuildRequires:	gtksourceview2-devel
+BuildRequires:	ocaml
+BuildRequires:	ocaml-lablgtk-devel
+BuildRequires:	ocaml-ocamlgraph-devel
+BuildRequires:	prelink
 
-# Still no ocaml on s390(x) or sparc64
-ExcludeArch: s390 s390x sparc64
+Requires(post): coreutils
 
-%description
+# This should always match the list in the ocaml spec file.
+ExclusiveArch: alpha armv4l %{ix86} ia64 x86_64 ppc sparc sparcv9 ppc64
 
+%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
@@ -38,6 +36,14 @@ 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
 
@@ -60,10 +66,11 @@ touch version.sh.in
 %endif
 
 make %{opt_option}
+make %{opt_option} gui
 
-mv CeCILL-C CeCILL-C.iso8859
-iconv -f ISO-8859-1 -t UTF-8 < CeCILL-C.iso8859 > CeCILL-C
-rm CeCILL-C.iso8859
+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
@@ -80,22 +87,51 @@ execstack -c ./alt-ergo.opt
 %{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}
+# 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
-%defattr(-,root,root,-)
-%{_bindir}/*
-%{_datadir}/%{name}
-%{_mandir}/man1/alt-ergo.1.gz
+%{_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
+* Thu May 12 2011 Jerry James <loganjerry at 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 at lists.fedoraproject.org> - 0.92.1-2
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
 
diff --git a/sources b/sources
index 2f67953..14e8bd7 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-4940caa641230c12c892262f91cb99b6  alt-ergo-0.92.1.tar.gz
+b58fdf53faf4c7b294a38c64176be2f3  alt-ergo-0.93.tar.gz