alt-ergo.spec

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