# 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.93 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 BuildRequires: gtksourceview2-devel BuildRequires: ocaml BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-ocamlgraph-devel BuildRequires: prelink Requires(post): coreutils # 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 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 cp -p %{SOURCE1} %{SOURCE2} . # 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} %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 # 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 # 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 %{_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@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 * 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.