]>
Commit | Line | Data |
---|---|---|
56491d8d JR |
1 | Summary: Software verification platform |
2 | Name: why3 | |
86ab24c9 | 3 | Version: 1.4.0 |
999402af | 4 | Release: 1 |
56491d8d | 5 | License: LGPLv2 with exceptions |
999402af | 6 | Group: Applications |
86ab24c9 JR |
7 | Source0: https://gforge.inria.fr/frs/download.php/38425/%{name}-%{version}.tar.gz |
8 | # Source0-md5: 9755cedf1edfcacff652149783e18647 | |
56491d8d JR |
9 | URL: http://why3.lri.fr/ |
10 | BuildRequires: camlp5 | |
86ab24c9 | 11 | BuildRequires: coq >= 8.13 |
56491d8d JR |
12 | BuildRequires: ocaml |
13 | BuildRequires: ocaml-findlib-devel | |
14 | BuildRequires: ocaml-graph-devel | |
86ab24c9 JR |
15 | BuildRequires: ocaml-lablgtk3-devel |
16 | BuildRequires: ocaml-lablgtk3-gtksourceview-devel | |
ab647362 | 17 | BuildRequires: ocaml-menhir-devel |
86ab24c9 | 18 | BuildRequires: ocaml-num-devel |
56491d8d | 19 | BuildRequires: ocaml-sqlite-devel |
b27c758f | 20 | BuildRequires: ocaml-zarith-devel |
56491d8d JR |
21 | BuildRequires: rubber |
22 | BuildRequires: sqlite3-devel | |
56491d8d | 23 | %requires_eq ocaml-runtime |
21bfd7ee JR |
24 | # same as ocaml-zarith |
25 | ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 | |
56491d8d JR |
26 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
27 | ||
28 | %description | |
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. | |
35 | ||
59fd71fc JR |
36 | %package examples |
37 | Summary: Example problems for why3 | |
38 | Group: Applications | |
39 | Requires: %{name} = %{version}-%{release} | |
40 | ||
41 | %description examples | |
42 | Example problems for why3. | |
43 | ||
56491d8d JR |
44 | %prep |
45 | %setup -q | |
46 | ||
47 | %build | |
48 | %configure \ | |
49 | --enable-doc | |
50 | ||
51 | %{__make} | |
52 | ||
53 | %install | |
54 | rm -rf $RPM_BUILD_ROOT | |
86ab24c9 | 55 | install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} |
56491d8d JR |
56 | |
57 | %{__make} install \ | |
58 | DESTDIR=$RPM_BUILD_ROOT | |
59 | ||
60 | # Move the gtksourceview language file to the right place | |
86ab24c9 JR |
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 | |
56491d8d | 63 | |
86ab24c9 | 64 | cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} |
59fd71fc | 65 | |
56491d8d JR |
66 | %clean |
67 | rm -rf $RPM_BUILD_ROOT | |
68 | ||
69 | %files | |
70 | %defattr(644,root,root,755) | |
86ab24c9 | 71 | %doc CHANGES.md README.md |
56491d8d JR |
72 | %attr(755,root,root) %{_bindir}/%{name}* |
73 | %{_datadir}/%{name} | |
86ab24c9 JR |
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 | |
14e36670 JR |
77 | %dir %{_libdir}/%{name} |
78 | %{_libdir}/%{name}/coq | |
14e36670 | 79 | %{_libdir}/%{name}/plugins |
999402af | 80 | %dir %{_libdir}/%{name}/commands |
86ab24c9 | 81 | %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs |
14e36670 | 82 | %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs |
86ab24c9 JR |
83 | %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit |
84 | %attr(755,root,root) %{_libdir}/%{name}/why3server | |
59fd71fc JR |
85 | |
86 | %files examples | |
87 | %defattr(644,root,root,755) | |
88 | %{_examplesdir}/%{name}-%{version} |