1 Summary: Software verification platform
5 License: LGPLv2 with exceptions
7 Source0: https://gforge.inria.fr/frs/download.php/36398/%{name}-%{version}.tar.gz
8 # Source0-md5: ea24a4877ca09e2ec4fff19d5f4d35c6
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-menhir
20 BuildRequires: ocaml-menhir-devel
21 BuildRequires: ocaml-sqlite-devel
22 BuildRequires: ocaml-zarith-devel
24 BuildRequires: sqlite3-devel
25 Requires: gtksourceview2
26 %requires_eq ocaml-runtime
27 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
30 Why3 is the next generation of the Why software verification platform.
31 Why3 clearly separates the purely logical specification part from
32 generation of verification conditions for programs. It features a rich
33 library of proof task transformations that can be chained to produce a
34 suitable input for a large set of theorem provers, including SMT
35 solvers, TPTP provers, as well as interactive proof assistants.
38 Summary: Example problems for why3
40 Requires: %{name} = %{version}-%{release}
43 Example problems for why3.
55 rm -rf $RPM_BUILD_ROOT
56 install -d $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
59 DESTDIR=$RPM_BUILD_ROOT
61 # Move the gtksourceview language file to the right place
62 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-2.0
63 mv $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-2.0/language-specs
65 cp -a examples/* $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
68 rm -rf $RPM_BUILD_ROOT
71 %defattr(644,root,root,755)
72 %doc LICENSE README doc/manual.pdf
73 %attr(755,root,root) %{_bindir}/%{name}*
75 %{_datadir}/gtksourceview-2.0/language-specs/why3.lang
76 %dir %{_libdir}/%{name}
77 %{_libdir}/%{name}/coq
78 %{_libdir}/%{name}/coq-tactic
79 %{_libdir}/%{name}/plugins
80 %dir %{_libdir}/%{name}/commands
81 %attr(755,root,root) %{_libdir}/why3/commands/why3config
82 %attr(755,root,root) %{_libdir}/why3/commands/why3doc
83 %attr(755,root,root) %{_libdir}/why3/commands/why3execute
84 %attr(755,root,root) %{_libdir}/why3/commands/why3extract
85 %attr(755,root,root) %{_libdir}/why3/commands/why3ide
86 %attr(755,root,root) %{_libdir}/why3/commands/why3prove
87 %attr(755,root,root) %{_libdir}/why3/commands/why3realize
88 %attr(755,root,root) %{_libdir}/why3/commands/why3replay
89 %attr(755,root,root) %{_libdir}/why3/commands/why3session
90 %attr(755,root,root) %{_libdir}/why3/commands/why3wc
91 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
92 %attr(755,root,root) %{_libdir}/%{name}/why3-cpulimit
95 %defattr(644,root,root,755)
96 %{_examplesdir}/%{name}-%{version}