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