]>
Commit | Line | Data |
---|---|---|
56491d8d JR |
1 | Summary: Software verification platform |
2 | Name: why3 | |
86ab24c9 | 3 | Version: 1.4.0 |
8f12d2a9 | 4 | Release: 4 |
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 | ||
d9dd4fa0 JR |
28 | %define _noautoreq ocamlx?\\\(Why3\\\) |
29 | ||
56491d8d JR |
30 | %description |
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. | |
37 | ||
59fd71fc JR |
38 | %package examples |
39 | Summary: Example problems for why3 | |
40 | Group: Applications | |
41 | Requires: %{name} = %{version}-%{release} | |
42 | ||
43 | %description examples | |
44 | Example problems for why3. | |
45 | ||
56491d8d JR |
46 | %prep |
47 | %setup -q | |
48 | ||
49 | %build | |
50 | %configure \ | |
51 | --enable-doc | |
52 | ||
53 | %{__make} | |
54 | ||
55 | %install | |
56 | rm -rf $RPM_BUILD_ROOT | |
86ab24c9 | 57 | install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} |
56491d8d JR |
58 | |
59 | %{__make} install \ | |
60 | DESTDIR=$RPM_BUILD_ROOT | |
61 | ||
62 | # Move the gtksourceview language file to the right place | |
86ab24c9 JR |
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 | |
56491d8d | 65 | |
86ab24c9 | 66 | cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} |
59fd71fc | 67 | |
56491d8d JR |
68 | %clean |
69 | rm -rf $RPM_BUILD_ROOT | |
70 | ||
71 | %files | |
72 | %defattr(644,root,root,755) | |
86ab24c9 | 73 | %doc CHANGES.md README.md |
56491d8d JR |
74 | %attr(755,root,root) %{_bindir}/%{name}* |
75 | %{_datadir}/%{name} | |
86ab24c9 JR |
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 | |
14e36670 JR |
79 | %dir %{_libdir}/%{name} |
80 | %{_libdir}/%{name}/coq | |
14e36670 | 81 | %{_libdir}/%{name}/plugins |
999402af | 82 | %dir %{_libdir}/%{name}/commands |
86ab24c9 | 83 | %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs |
14e36670 | 84 | %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs |
86ab24c9 JR |
85 | %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit |
86 | %attr(755,root,root) %{_libdir}/%{name}/why3server | |
59fd71fc JR |
87 | |
88 | %files examples | |
89 | %defattr(644,root,root,755) | |
90 | %{_examplesdir}/%{name}-%{version} |