alt-ergo.spec

   1 Summary:        Automated theorem prover including linear arithmetic
   2 Name:           alt-ergo
   3 Version:        0.95.2
   4 Release:        1
   5 License:        CeCILL-C
   6 Group:          Applications/Engineering
   7 URL:            http://alt-ergo.lri.fr/
   8 Source0:        http://alt-ergo.ocamlpro.com/http/%{name}-%{version}/alt-ergo-%{version}.tar.gz
   9 # Source0-md5:  ab9c160f7ecb26aa2479f9169db9b869
  10 Source1:        %{name}.desktop
  11 BuildRequires:  desktop-file-utils
  12 BuildRequires:  gtksourceview2-devel
  13 BuildRequires:  iconv
  14 BuildRequires:  ocaml
  15 BuildRequires:  ocaml-graph-devel
  16 BuildRequires:  ocaml-lablgtk2-devel
  17 BuildRequires:  ocaml-lablgtk2-gtksourceview2-devel
  18 BuildRequires:  ocaml-zarith-devel
  19 Requires(post): coreutils
  20 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  21
  22 %description
  23 Alt-Ergo is an automated theorem prover implemented in OCaml. It is
  24 based on CC(X) - a congruence closure algorithm parameterized by an
  25 equational theory X. This algorithm is reminiscent of the Shostak
  26 algorithm. Currently CC(X) is instantiated by the theory of linear
  27 arithmetics. Alt-Ergo also contains a home made SAT-solver and an
  28 instantiation mechanism by which it fully supports quantifiers.
  29
  30 %package gui
  31 Summary:        Graphical front end for alt-ergo
  32 Group:          Applications/Engineering
  33 Requires:       %{name}%{?_isa} = %{version}-%{release}
  34 Requires:       gtksourceview2
  35
  36 %description gui
  37 A graphical front end for the alt-ergo theorem prover.
  38
  39 %prep
  40 %setup -q
  41
  42 # Set print_flag to false or invoking with -select
  43 # from "why" will pause every invocation :-(.
  44 sed -i -e 's/let print_flag = true/let print_flag = false/;' src/preprocess/pruning.ml
  45
  46 %build
  47 ./configure \
  48         --prefix=%{_prefix} \
  49         --bindir=%{_bindir} \
  50         --libdir=%{_datadir} \
  51         --mandir=%{_mandir}
  52
  53 %{__make} -j1 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
  54 %{__make} -j1 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt gui
  55
  56 %install
  57 rm -rf $RPM_BUILD_ROOT
  58 install -d $RPM_BUILD_ROOT{%{_bindir},%{_desktopdir}}
  59
  60 %{__make} install install-gui \
  61         OCAMLBEST=opt OCAMLOPT=ocamlopt.opt \
  62         DESTDIR=$RPM_BUILD_ROOT
  63
  64 # Remove files we do not want installed
  65 rm -f $RPM_BUILD_ROOT%{_datadir}/%{name}/*.{cmx,o}
  66
  67 # Install the desktop file
  68 desktop-file-install --dir $RPM_BUILD_ROOT%{_desktopdir} %{SOURCE1}
  69
  70 %clean
  71 rm -rf $RPM_BUILD_ROOT
  72
  73 %post gui
  74 %update_desktop_database
  75
  76 %postun gui
  77 %update_desktop_database
  78
  79 %files
  80 %defattr(644,root,root,755)
  81 %attr(755,root,root) %{_bindir}/%{name}
  82 %{_mandir}/man1/alt-ergo.1.*
  83 %doc COPYING CHANGES
  84
  85 %files gui
  86 %defattr(644,root,root,755)
  87 %attr(755,root,root) %{_bindir}/altgr-ergo
  88 %{_desktopdir}/%{name}.desktop
  89 %{_datadir}/gtksourceview-2.0/language-specs/%{name}.lang