1 Summary: Software verification platform
6 License: LGPLv2 with exceptions
7 Source0: https://gforge.inria.fr/frs/download.php/33490/%{name}-%{version}.tar.gz
8 # Source0-md5: 35f99e5f64939e50ea57f641ba2073ec
9 URL: http://why3.lri.fr/
11 BuildRequires: coq >= 8.4
13 BuildRequires: gtksourceview2-devel
15 BuildRequires: ocaml-findlib-devel
16 BuildRequires: ocaml-graph-devel
17 BuildRequires: ocaml-lablgtk2-devel
18 BuildRequires: ocaml-lablgtk2-gtksourceview2-devel
19 BuildRequires: ocaml-sqlite-devel
20 BuildRequires: ocaml-zarith-devel
22 BuildRequires: sqlite3-devel
23 Requires: gtksourceview2
24 %requires_eq ocaml-runtime
25 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
28 Why3 is the next generation of the Why software verification platform.
29 Why3 clearly separates the purely logical specification part from
30 generation of verification conditions for programs. It features a rich
31 library of proof task transformations that can be chained to produce a
32 suitable input for a large set of theorem provers, including SMT
33 solvers, TPTP provers, as well as interactive proof assistants.
36 Summary: Example problems for why3
38 Requires: %{name} = %{version}-%{release}
41 Example problems for why3.
53 rm -rf $RPM_BUILD_ROOT
54 install -d $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
57 DESTDIR=$RPM_BUILD_ROOT
59 # Move the gtksourceview language file to the right place
60 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-2.0
61 mv $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-2.0/language-specs
63 cp -a examples/* $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
66 rm -rf $RPM_BUILD_ROOT
69 %defattr(644,root,root,755)
70 %doc LICENSE README doc/manual.pdf
71 %attr(755,root,root) %{_bindir}/%{name}*
73 %{_datadir}/gtksourceview-2.0/language-specs/why3.lang
74 %dir %{_libdir}/%{name}
75 %{_libdir}/%{name}/coq
76 %{_libdir}/%{name}/coq-tactic
77 %{_libdir}/%{name}/plugins
78 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
79 %attr(755,root,root) %{_libdir}/%{name}/why3-cpulimit
82 %defattr(644,root,root,755)
83 %{_examplesdir}/%{name}-%{version}