]>
Commit | Line | Data |
---|---|---|
56491d8d JR |
1 | Summary: Software verification platform |
2 | Name: why3 | |
b27c758f JR |
3 | Version: 0.83 |
4 | Release: 1 | |
56491d8d JR |
5 | Group: Applications |
6 | License: LGPLv2 with exceptions | |
b27c758f JR |
7 | Source0: https://gforge.inria.fr/frs/download.php/33490/%{name}-%{version}.tar.gz |
8 | # Source0-md5: 35f99e5f64939e50ea57f641ba2073ec | |
56491d8d JR |
9 | URL: http://why3.lri.fr/ |
10 | BuildRequires: camlp5 | |
b27c758f | 11 | BuildRequires: coq >= 8.4 |
56491d8d JR |
12 | BuildRequires: evince |
13 | BuildRequires: gtksourceview2-devel | |
14 | BuildRequires: ocaml | |
15 | BuildRequires: ocaml-findlib-devel | |
16 | BuildRequires: ocaml-graph-devel | |
6c13c319 JR |
17 | BuildRequires: ocaml-lablgtk2-devel |
18 | BuildRequires: ocaml-lablgtk2-gtksourceview2-devel | |
56491d8d | 19 | BuildRequires: ocaml-sqlite-devel |
b27c758f | 20 | BuildRequires: ocaml-zarith-devel |
56491d8d JR |
21 | BuildRequires: rubber |
22 | BuildRequires: sqlite3-devel | |
56491d8d JR |
23 | Requires: gtksourceview2 |
24 | %requires_eq ocaml-runtime | |
25 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) | |
26 | ||
27 | %description | |
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. | |
34 | ||
59fd71fc JR |
35 | %package examples |
36 | Summary: Example problems for why3 | |
37 | Group: Applications | |
38 | Requires: %{name} = %{version}-%{release} | |
39 | ||
40 | %description examples | |
41 | Example problems for why3. | |
42 | ||
56491d8d JR |
43 | %prep |
44 | %setup -q | |
45 | ||
46 | %build | |
47 | %configure \ | |
48 | --enable-doc | |
49 | ||
50 | %{__make} | |
51 | ||
52 | %install | |
53 | rm -rf $RPM_BUILD_ROOT | |
59fd71fc | 54 | install -d $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version} |
56491d8d JR |
55 | |
56 | %{__make} install \ | |
57 | DESTDIR=$RPM_BUILD_ROOT | |
58 | ||
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 | |
62 | ||
59fd71fc JR |
63 | cp -a examples/* $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version} |
64 | ||
56491d8d JR |
65 | %clean |
66 | rm -rf $RPM_BUILD_ROOT | |
67 | ||
68 | %files | |
69 | %defattr(644,root,root,755) | |
70 | %doc LICENSE README doc/manual.pdf | |
71 | %attr(755,root,root) %{_bindir}/%{name}* | |
72 | %{_datadir}/%{name} | |
b27c758f | 73 | %{_datadir}/gtksourceview-2.0/language-specs/why3.lang |
56491d8d | 74 | %{_libdir}/%{name} |
59fd71fc JR |
75 | |
76 | %files examples | |
77 | %defattr(644,root,root,755) | |
78 | %{_examplesdir}/%{name}-%{version} |