1 Summary: Automated theorem prover including linear arithmetic
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
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)
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.
31 Summary: Graphical front end for alt-ergo
32 Group: Applications/Engineering
33 Requires: %{name}%{?_isa} = %{version}-%{release}
34 Requires: gtksourceview2
37 A graphical front end for the alt-ergo theorem prover.
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
50 --libdir=%{_datadir} \
53 %{__make} -j1 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
54 %{__make} -j1 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt gui
57 rm -rf $RPM_BUILD_ROOT
58 install -d $RPM_BUILD_ROOT{%{_bindir},%{_desktopdir}}
60 %{__make} install install-gui \
61 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt \
62 DESTDIR=$RPM_BUILD_ROOT
64 # Remove files we do not want installed
65 rm -f $RPM_BUILD_ROOT%{_datadir}/%{name}/*.{cmx,o}
67 # Install the desktop file
68 desktop-file-install --dir $RPM_BUILD_ROOT%{_desktopdir} %{SOURCE1}
71 rm -rf $RPM_BUILD_ROOT
74 %update_desktop_database
77 %update_desktop_database
80 %defattr(644,root,root,755)
81 %attr(755,root,root) %{_bindir}/%{name}
82 %{_mandir}/man1/alt-ergo.1.*
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