- release 5 (by relup.sh)

[packages/why3.git] / why3.spec

diff --git a/why3.spec b/why3.spec
index 53c1153dc953d875e404da609fdfa358f2ec2bd6..2ea96b2fd41a14910dee7e7aa26078f7c0a6359f 100644 (file)
--- a/why3.spec
+++ b/why3.spec
@@ -1,14 +1,14 @@
 Summary:       Software verification platform
 Name:          why3
-Version:       0.73
-Release:       1
+Version:       0.83
+Release:       5
 Group:         Applications
 License:       LGPLv2 with exceptions
-Source0:       https://gforge.inria.fr/frs/download.php/31257/%{name}-%{version}.tar.gz
-# Source0-md5: 8994f147b7fc4084da46e81693e044bb
+Source0:       https://gforge.inria.fr/frs/download.php/33490/%{name}-%{version}.tar.gz
+# Source0-md5: 35f99e5f64939e50ea57f641ba2073ec
 URL:           http://why3.lri.fr/
 BuildRequires: camlp5
-BuildRequires: coq
+BuildRequires: coq >= 8.4
 BuildRequires: evince
 BuildRequires: gtksourceview2-devel
 BuildRequires: ocaml
@@ -17,6 +17,7 @@ BuildRequires:        ocaml-graph-devel
 BuildRequires: ocaml-lablgtk2-devel
 BuildRequires: ocaml-lablgtk2-gtksourceview2-devel
 BuildRequires: ocaml-sqlite-devel
+BuildRequires: ocaml-zarith-devel
 BuildRequires: rubber
 BuildRequires: sqlite3-devel
 Requires:      gtksourceview2
@@ -31,6 +32,14 @@ library of proof task transformations that can be chained to produce a
 suitable input for a large set of theorem provers, including SMT
 solvers, TPTP provers, as well as interactive proof assistants.
 
+%package examples
+Summary:       Example problems for why3
+Group:         Applications
+Requires:      %{name} = %{version}-%{release}
+
+%description examples
+Example problems for why3.
+
 %prep
 %setup -q
 
@@ -42,6 +51,7 @@ solvers, TPTP provers, as well as interactive proof assistants.
 
 %install
 rm -rf $RPM_BUILD_ROOT
+install -d $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
 
 %{__make} install \
        DESTDIR=$RPM_BUILD_ROOT
@@ -50,6 +60,8 @@ rm -rf $RPM_BUILD_ROOT
 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-2.0
 mv $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-2.0/language-specs
 
+cp -a examples/* $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
+
 %clean
 rm -rf $RPM_BUILD_ROOT
 
@@ -58,5 +70,14 @@ rm -rf $RPM_BUILD_ROOT
 %doc LICENSE README doc/manual.pdf
 %attr(755,root,root) %{_bindir}/%{name}*
 %{_datadir}/%{name}
-%{_datadir}/gtksourceview-2.0/language-specs/why.lang
-%{_libdir}/%{name}
+%{_datadir}/gtksourceview-2.0/language-specs/why3.lang
+%dir %{_libdir}/%{name}
+%{_libdir}/%{name}/coq
+%{_libdir}/%{name}/coq-tactic
+%{_libdir}/%{name}/plugins
+%attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
+%attr(755,root,root) %{_libdir}/%{name}/why3-cpulimit
+
+%files examples
+%defattr(644,root,root,755)
+%{_examplesdir}/%{name}-%{version}