]>
Commit | Line | Data |
---|---|---|
56491d8d JR |
1 | Summary: Software verification platform |
2 | Name: why3 | |
ab647362 JR |
3 | Version: 0.87.3 |
4 | Release: 0.1 | |
56491d8d JR |
5 | Group: Applications |
6 | License: LGPLv2 with exceptions | |
ab647362 JR |
7 | Source0: https://gforge.inria.fr/frs/download.php/36398/%{name}-%{version}.tar.gz |
8 | # Source0-md5: ea24a4877ca09e2ec4fff19d5f4d35c6 | |
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 | |
ab647362 JR |
19 | BuildRequires: ocaml-menhir |
20 | BuildRequires: ocaml-menhir-devel | |
56491d8d | 21 | BuildRequires: ocaml-sqlite-devel |
b27c758f | 22 | BuildRequires: ocaml-zarith-devel |
56491d8d JR |
23 | BuildRequires: rubber |
24 | BuildRequires: sqlite3-devel | |
56491d8d JR |
25 | Requires: gtksourceview2 |
26 | %requires_eq ocaml-runtime | |
27 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) | |
28 | ||
29 | %description | |
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. | |
36 | ||
59fd71fc JR |
37 | %package examples |
38 | Summary: Example problems for why3 | |
39 | Group: Applications | |
40 | Requires: %{name} = %{version}-%{release} | |
41 | ||
42 | %description examples | |
43 | Example problems for why3. | |
44 | ||
56491d8d JR |
45 | %prep |
46 | %setup -q | |
47 | ||
48 | %build | |
49 | %configure \ | |
50 | --enable-doc | |
51 | ||
52 | %{__make} | |
53 | ||
54 | %install | |
55 | rm -rf $RPM_BUILD_ROOT | |
59fd71fc | 56 | install -d $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version} |
56491d8d JR |
57 | |
58 | %{__make} install \ | |
59 | DESTDIR=$RPM_BUILD_ROOT | |
60 | ||
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 | |
64 | ||
59fd71fc JR |
65 | cp -a examples/* $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version} |
66 | ||
56491d8d JR |
67 | %clean |
68 | rm -rf $RPM_BUILD_ROOT | |
69 | ||
70 | %files | |
71 | %defattr(644,root,root,755) | |
72 | %doc LICENSE README doc/manual.pdf | |
73 | %attr(755,root,root) %{_bindir}/%{name}* | |
74 | %{_datadir}/%{name} | |
b27c758f | 75 | %{_datadir}/gtksourceview-2.0/language-specs/why3.lang |
14e36670 JR |
76 | %dir %{_libdir}/%{name} |
77 | %{_libdir}/%{name}/coq | |
78 | %{_libdir}/%{name}/coq-tactic | |
79 | %{_libdir}/%{name}/plugins | |
80 | %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs | |
81 | %attr(755,root,root) %{_libdir}/%{name}/why3-cpulimit | |
59fd71fc JR |
82 | |
83 | %files examples | |
84 | %defattr(644,root,root,755) | |
85 | %{_examplesdir}/%{name}-%{version} |