1 Summary: Software verification platform
5 License: LGPLv2 with exceptions
7 Source0: https://gforge.inria.fr/frs/download.php/38425/%{name}-%{version}.tar.gz
8 # Source0-md5: 9755cedf1edfcacff652149783e18647
9 URL: http://why3.lri.fr/
11 BuildRequires: coq >= 8.13
13 BuildRequires: ocaml-findlib-devel
14 BuildRequires: ocaml-graph-devel
15 BuildRequires: ocaml-lablgtk3-devel
16 BuildRequires: ocaml-lablgtk3-gtksourceview-devel
17 BuildRequires: ocaml-menhir-devel
18 BuildRequires: ocaml-num-devel
19 BuildRequires: ocaml-sqlite-devel
20 BuildRequires: ocaml-zarith-devel
22 BuildRequires: sqlite3-devel
23 %requires_eq ocaml-runtime
24 # same as ocaml-zarith
25 ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
26 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
29 Why3 is the next generation of the Why software verification platform.
30 Why3 clearly separates the purely logical specification part from
31 generation of verification conditions for programs. It features a rich
32 library of proof task transformations that can be chained to produce a
33 suitable input for a large set of theorem provers, including SMT
34 solvers, TPTP provers, as well as interactive proof assistants.
37 Summary: Example problems for why3
39 Requires: %{name} = %{version}-%{release}
42 Example problems for why3.
54 rm -rf $RPM_BUILD_ROOT
55 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
58 DESTDIR=$RPM_BUILD_ROOT
60 # Move the gtksourceview language file to the right place
61 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0
62 %{__mv} $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0/language-specs
64 cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
67 rm -rf $RPM_BUILD_ROOT
70 %defattr(644,root,root,755)
71 %doc CHANGES.md README.md
72 %attr(755,root,root) %{_bindir}/%{name}*
74 %{_datadir}/gtksourceview-3.0/language-specs/why3.lang
75 %{_datadir}/gtksourceview-3.0/language-specs/why3c.lang
76 %{_datadir}/gtksourceview-3.0/language-specs/why3py.lang
77 %dir %{_libdir}/%{name}
78 %{_libdir}/%{name}/coq
79 %{_libdir}/%{name}/plugins
80 %dir %{_libdir}/%{name}/commands
81 %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs
82 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
83 %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit
84 %attr(755,root,root) %{_libdir}/%{name}/why3server
87 %defattr(644,root,root,755)
88 %{_examplesdir}/%{name}-%{version}