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