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)
28 %define _noautoreq ocamlx?\\\(Why3\\\)
31 Why3 is the next generation of the Why software verification platform.
32 Why3 clearly separates the purely logical specification part from
33 generation of verification conditions for programs. It features a rich
34 library of proof task transformations that can be chained to produce a
35 suitable input for a large set of theorem provers, including SMT
36 solvers, TPTP provers, as well as interactive proof assistants.
39 Summary: Example problems for why3
41 Requires: %{name} = %{version}-%{release}
44 Example problems for why3.
56 rm -rf $RPM_BUILD_ROOT
57 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
60 DESTDIR=$RPM_BUILD_ROOT
62 # Move the gtksourceview language file to the right place
63 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0
64 %{__mv} $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0/language-specs
66 cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
69 rm -rf $RPM_BUILD_ROOT
72 %defattr(644,root,root,755)
73 %doc CHANGES.md README.md
74 %attr(755,root,root) %{_bindir}/%{name}*
76 %{_datadir}/gtksourceview-3.0/language-specs/why3.lang
77 %{_datadir}/gtksourceview-3.0/language-specs/why3c.lang
78 %{_datadir}/gtksourceview-3.0/language-specs/why3py.lang
79 %dir %{_libdir}/%{name}
80 %{_libdir}/%{name}/coq
81 %{_libdir}/%{name}/plugins
82 %dir %{_libdir}/%{name}/commands
83 %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs
84 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
85 %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit
86 %attr(755,root,root) %{_libdir}/%{name}/why3server
89 %defattr(644,root,root,755)
90 %{_examplesdir}/%{name}-%{version}