# 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. %global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) %if !%{opt} %global debug_package %{nil} %endif Name: alt-ergo Version: 1.30 Release: 12%{?dist} Summary: Automated theorem prover including linear arithmetic License: CeCILL-C URL: http://alt-ergo.ocamlpro.com/ Source0: http://alt-ergo.ocamlpro.com/http/%{name}-%{version}/%{name}-%{version}.tar.gz # Created with gimp from official upstream icon Source1: %{name}-icons.tar.xz Source2: %{name}.desktop Source3: %{name}.appdata.xml # Use the asmrun_pic variant when linking the binary. Patch1: alt-ergo-1.30-use-pic.patch BuildRequires: desktop-file-utils BuildRequires: gtksourceview2-devel BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocamlgraph-devel BuildRequires: ocaml-ocplib-simplex-devel BuildRequires: ocaml-zarith-devel BuildRequires: ocaml-zip-devel %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 Requires: %{name}%{?_isa} = %{version}-%{release} Requires: gtksourceview2 Requires: hicolor-icon-theme Requires(post): coreutils Requires(postun): coreutils %description gui A graphical front end for the alt-ergo theorem prover. %prep %setup -q %setup -q -T -D -a 1 %patch1 -p1 cp -p %{SOURCE2} . # Fix encoding iconv -f ISO-8859-1 -t UTF-8 -o LICENSE.utf8 LICENSE touch -r LICENSE LICENSE.utf8 mv -f LICENSE.utf8 LICENSE # Use Fedora LDFLAGS sed -i "s|^OFLAGS =.*|& -g|" Makefile.users for arg in $RPM_LD_FLAGS; do sed -i "s|^OFLAGS =.*-g|& -ccopt $arg|" Makefile.users done %build %configure %if ! %{opt} %global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLLEX=ocamllex %else %global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt %endif make %{opt_option} make %{opt_option} gui %install mkdir -p %{buildroot}%{_bindir} make %{opt_option} DESTDIR=%{buildroot} install install-gui # Move the gtksourceview file to the right place mv %{buildroot}%{_datadir}/%{name}/gtksourceview-2.0 %{buildroot}%{_datadir} rmdir %{buildroot}%{_datadir}/%{name} # Install the desktop file mkdir -p %{buildroot}%{_datadir}/applications desktop-file-install --dir %{buildroot}%{_datadir}/applications %{name}.desktop # Install the AppData file mkdir -p %{buildroot}%{_datadir}/appdata install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata # Install the icons mkdir -p %{buildroot}%{_datadir}/icons cp -a icons %{buildroot}%{_datadir}/icons/hicolor %check # Test alt-ergo on the examples. %define altergo %{buildroot}%{_bindir}/alt-ergo cd examples/valid for fil in *.why; do if ! %{altergo} $fil | grep -Fq Valid; then echo $fil was not found valid exit 1 fi done cd ../invalid for fil in *.why; do if %{altergo} $fil | grep -Fq Valid; then echo $fil was erroneously found valid exit 1 fi done %files %doc README.md CHANGES examples %license COPYING.md LICENSE %{_bindir}/%{name} %{_mandir}/man1/alt-ergo.1.* %files gui %{_bindir}/altgr-ergo %{_datadir}/appdata/%{name}.appdata.xml %{_datadir}/applications/%{name}.desktop %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang %{_datadir}/icons/hicolor/*/apps/%{name}.png %changelog * Wed Feb 07 2018 Fedora Release Engineering - 1.30-12 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild * Sun Jan 07 2018 Igor Gnatenko - 1.30-11 - Remove obsolete scriptlets * Wed Nov 08 2017 Richard W.M. Jones - 1.30-10 - OCaml 4.06.0 rebuild. * Mon Aug 07 2017 Richard W.M. Jones - 1.30-9 - OCaml 4.05.0 rebuild. * Wed Aug 02 2017 Fedora Release Engineering - 1.30-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild * Wed Jul 26 2017 Fedora Release Engineering - 1.30-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild * Mon Jun 26 2017 Richard W.M. Jones - 1.30-6 - OCaml 4.04.2 rebuild. * Fri May 12 2017 Richard W.M. Jones - 1.30-5 - Bump release and rebuild. * Fri May 12 2017 Richard W.M. Jones - 1.30-4 - Bump release and rebuild. * Fri May 12 2017 Richard W.M. Jones - 1.30-3 - OCaml 4.04.1 rebuild. * Fri Feb 10 2017 Fedora Release Engineering - 1.30-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild * Mon Nov 28 2016 Jerry James - 1.30-1 - Update to version 1.30 * Mon Nov 07 2016 Richard W.M. Jones - 1.01-3 - Rebuild for OCaml 4.04.0. * Sat Apr 16 2016 Jerry James - 1.01-2 - Rebuild for ocaml-ocamlgraph 1.8.7 * Wed Feb 17 2016 Jerry James - 1.01-1 - Update to version 1.01 * Wed Feb 03 2016 Fedora Release Engineering - 0.99.1-10 - Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild * Wed Nov 25 2015 Jerry James - 0.99.1-9 - Rebuild for zarith 1.4.1 * Tue Jul 28 2015 Richard W.M. Jones - 0.99.1-8 - OCaml 4.02.3 rebuild. * Wed Jun 24 2015 Richard W.M. Jones - 0.99.1-7 - ocaml-4.02.2 final rebuild. * Wed Jun 17 2015 Richard W.M. Jones - 0.99.1-6 - ocaml-4.02.2 rebuild. * Tue Jun 16 2015 Fedora Release Engineering - 0.99.1-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild * Wed Mar 18 2015 Jerry James - 0.99.1-4 - Rebuild for ocaml-ocamlgraph 1.8.6 * Fri Mar 13 2015 Jerry James - 0.99.1-3 - Fix FTBFS (bz 1099153) * Wed Feb 18 2015 Richard W.M. Jones - 0.99.1-2 - ocaml-4.02.1 rebuild. * Tue Jan 6 2015 Jerry James - 0.99.1-1 - Update to version 0.99.1 * Thu Oct 30 2014 Jerry James - 0.95.2-14 - Rebuild for new ocaml-lablgtk * Tue Oct 14 2014 Jerry James - 0.95.2-13 - Rebuild for ocaml-zarith 1.3 - Fix license handling * Tue Sep 2 2014 Jerry James - 0.95.2-12 - ocaml-4.02.0 final rebuild. * Sat Aug 23 2014 Richard W.M. Jones - 0.95.2-11 - ocaml-4.02.0+rc1 rebuild. * Fri Aug 15 2014 Fedora Release Engineering - 0.95.2-10 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild * Sat Aug 02 2014 Richard W.M. Jones - 0.95.2-9 - ocaml-4.02.0-0.8.git10e45753.fc22 rebuild. * Fri Jul 25 2014 Richard W.M. Jones - 0.95.2-8 - Bump release and rebuild. * Fri Jul 25 2014 Richard W.M. Jones - 0.95.2-7 - Rebuild for OCaml 4.02.0 beta. * Sat Jun 07 2014 Fedora Release Engineering - 0.95.2-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild * Mon Apr 21 2014 Jerry James - 0.95.2-5 - Rebuild for ocamlgraph 1.8.5 * Tue Apr 15 2014 Richard W.M. Jones - 0.95.2-4 - Remove ocaml_arches macro (RHBZ#1087794). * Mon Mar 24 2014 Jerry James - 0.95.2-3 - Add desktop icons - Drop unnecessary gmp-devel BR (pulled in by ocaml-zarith-devel) - Fix bytecode build - Drop screenshot, now hosted externally * Tue Mar 4 2014 Jerry James - 0.95.2-2 - Add an AppData file and screenshot - Adapt to ocamlgraph 1.8.4 * Fri Sep 20 2013 Jerry James - 0.95.2-1 - Update to version 0.95.2 - Web pages and downloads now hosted by ocamlpro.com - Add ocaml-findlib, ocaml-zarith, and gmp-devel BRs - Drop prelink BR; execstack is no longer set - Fix bogus changelog dates * Sat Sep 14 2013 Richard W.M. Jones - 0.95.1-4 - Rebuild for OCaml 4.01.0. - Enable debuginfo. - Change some define -> global. - Remove Group lines not needed by modern RPM. * Sat Aug 03 2013 Fedora Release Engineering - 0.95.1-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild * Tue May 14 2013 Jerry James - 0.95.1-2 - Rebuild for ocaml-ocamlgraph 1.8.3 - Make the binaries full RELRO due to network use * Tue Mar 5 2013 Jerry James - 0.95.1-1 - Update to version 0.95.1 - Drop upstreamed -install patch * Wed Feb 13 2013 Fedora Release Engineering - 0.95-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild * Mon Jan 14 2013 Jerry James - 0.95-1 - Update to version 0.95 - Add -install patch to fix installation failure * Wed Oct 17 2012 Jerry James - 0.94-7 - Rebuild for OCaml 4.00.1 * Mon Jul 30 2012 Jerry James - 0.94-6 - Rebuild for ocaml-ocamlgraph 1.8.2 * Wed Jul 18 2012 Fedora Release Engineering - 0.94-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild * Tue Jun 12 2012 Jerry James - 0.94-4 - Rebuild for OCaml 4.00.0 * Thu Jan 12 2012 Fedora Release Engineering - 0.94-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_17_Mass_Rebuild * Sat Jan 7 2012 Jerry James - 0.94-2 - Rebuild for OCaml 3.12.1 * Tue Dec 6 2011 Jerry James - 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 - 0.93-2 - Build on all arches with ocaml * Thu May 12 2011 Jerry James - 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 = in , let x = in - Partial support for the division operator - Unspecified bug fixes * Mon Feb 07 2011 Fedora Release Engineering - 0.92.1-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild * Wed Oct 06 2010 David A. Wheeler 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 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 0.9-2 - Added ExcludeArch sparc64 due to no OCaml * Fri Jul 24 2009 Alan Dunn 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 0.8-5.1 - ExcludeArch s390x as there's no ocaml available * Mon Feb 23 2009 Fedora Release Engineering - 0.8-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild * Wed Dec 24 2008 Alan Dunn 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 0.8-3 - Fixed BuildRequires to add prelink (for execstack). * Tue Aug 26 2008 Alan Dunn 0.8-2 - Fixed BuildRequires to add ocaml-ocamlgraph-devel instead of ocaml-ocamlgraph, made other minor changes. * Mon Aug 25 2008 Alan Dunn 0.8-1 - Initial Fedora RPM version.