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)
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))\\\)
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.
34 Summary: Graphical front end for alt-ergo
35 Group: Applications/Engineering
36 Requires: %{name}%{?_isa} = %{version}-%{release}
37 Requires: gtksourceview2
40 A graphical front end for the alt-ergo theorem prover.
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
53 --libdir=%{_datadir} \
56 %{__make} -j1 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
57 %{__make} -j1 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt gui
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
64 rm -rf $RPM_BUILD_ROOT
65 install -d $RPM_BUILD_ROOT{%{_bindir},%{_desktopdir}}
68 OCAMLBEST=opt OCAMLOPT=ocamlopt.opt \
69 DESTDIR=$RPM_BUILD_ROOT
71 # Remove files we do not want installed
72 rm -f $RPM_BUILD_ROOT%{_datadir}/%{name}/*.{cmx,o}
74 # Install the desktop file
75 desktop-file-install --dir $RPM_BUILD_ROOT%{_desktopdir} %{SOURCE1}
78 rm -rf $RPM_BUILD_ROOT
81 %update_desktop_database
84 %update_desktop_database
87 %defattr(644,root,root,755)
88 %attr(755,root,root) %{_bindir}/%{name}
90 %{_mandir}/man1/alt-ergo.1.*
91 %doc COPYING CeCILL-C CHANGES
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