[alt-ergo] Add a desktop file for the gui. Update to version 0.94. This means: - The theory of records replace

Tue Dec 6 16:06:18 UTC 2011

commit 0ed1c81296590044910c04b631e4655f90b9c6f4
Author: Jerry James <loganjerry at gmail.com>
Date:   Tue Dec 6 09:05:41 2011 -0700

    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

 .gitignore       |    2 +-
 alt-ergo.desktop |    9 ++++++
 alt-ergo.spec    |   77 ++++++++++++++++++++++++++++++++++-------------------
 sources          |    2 +-
 4 files changed, 60 insertions(+), 30 deletions(-)
---

diff --git a/.gitignore b/.gitignore
index dd524f0..c0b1c69 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/alt-ergo-0.93.tar.gz
+/alt-ergo-0.94.tar.gz
diff --git a/alt-ergo.desktop b/alt-ergo.desktop
new file mode 100644
index 0000000..5bd4cbf
--- /dev/null
+++ b/alt-ergo.desktop
@@ -0,0 +1,9 @@
+
+[Desktop Entry]
+Name=Alt-Ergo
+GenericName=theorem prover
+Comment=Automated theorem prover
+Exec=altgr-ergo %F
+Terminal=false
+Type=Application
+Categories=Development;Debugger;
diff --git a/alt-ergo.spec b/alt-ergo.spec
index f95eb65..c8b3f63 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -6,8 +6,8 @@
 %define debug_package %{nil}
 
 Name:		alt-ergo
-Version:	0.93
-Release:	2%{?dist}
+Version:	0.94
+Release:	1%{?dist}
 Summary:	Automated theorem prover including linear arithmetic
 
 Group:		Applications/Engineering
@@ -16,16 +16,22 @@ 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
+Requires(post):	coreutils
 
-ExclusiveArch:  %{ocaml_arches}
+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
@@ -39,6 +45,7 @@ instantiation mechanism by which it fully supports quantifiers.
 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.
@@ -46,16 +53,13 @@ A graphical front end for the alt-ergo theorem prover.
 %prep
 %setup -q
 
-cp -p %{SOURCE1} %{SOURCE2} .
+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
-# 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}
@@ -76,19 +80,13 @@ 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
 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
@@ -96,30 +94,53 @@ 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}
+
+# 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
-if [ -d %{_datadir}/gtksourceview-2.0/language-specs ]; then
-  cp -p %{_datadir}/%{name}/alt-ergo.lang \
-	%{_datadir}/gtksourceview-2.0/language-specs
-fi
+update-desktop-database &> /dev/null || :
 
-%triggerun gui -- gtksourceview2
-rm -f %{_datadir}/gtksourceview-2.0/language-specs/alt-ergo.lang
+%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}
-%dir %{_datadir}/%{name}
-%{_datadir}/%{name}/smt_prelude.mlw
+%{_datadir}/%{name}/
 %{_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
+%{_datadir}/applications/%{name}.desktop
+%{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang
 
 %changelog
+* Tue Dec  6 2011 Jerry James <loganjerry at 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 at gmail.com> - 0.93-2
 - Build on all arches with ocaml
 
diff --git a/sources b/sources
index 14e8bd7..34115ac 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-b58fdf53faf4c7b294a38c64176be2f3  alt-ergo-0.93.tar.gz
+796450fa0743c2205d729ccd246c6c17  alt-ergo-0.94.tar.gz
