why3.spec

   1 Summary:        Software verification platform
   2 Name:           why3
   3 Version:        0.83
   4 Release:        4
   5 Group:          Applications
   6 License:        LGPLv2 with exceptions
   7 Source0:        https://gforge.inria.fr/frs/download.php/33490/%{name}-%{version}.tar.gz
   8 # Source0-md5:  35f99e5f64939e50ea57f641ba2073ec
   9 URL:            http://why3.lri.fr/
  10 BuildRequires:  camlp5
  11 BuildRequires:  coq >= 8.4
  12 BuildRequires:  evince
  13 BuildRequires:  gtksourceview2-devel
  14 BuildRequires:  ocaml
  15 BuildRequires:  ocaml-findlib-devel
  16 BuildRequires:  ocaml-graph-devel
  17 BuildRequires:  ocaml-lablgtk2-devel
  18 BuildRequires:  ocaml-lablgtk2-gtksourceview2-devel
  19 BuildRequires:  ocaml-sqlite-devel
  20 BuildRequires:  ocaml-zarith-devel
  21 BuildRequires:  rubber
  22 BuildRequires:  sqlite3-devel
  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
  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
  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
  54 install -d $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
  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
  63 cp -a examples/* $RPM_BUILD_ROOT/%{_examplesdir}/%{name}-%{version}
  64
  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}
  73 %{_datadir}/gtksourceview-2.0/language-specs/why3.lang
  74 %dir %{_libdir}/%{name}
  75 %{_libdir}/%{name}/coq
  76 %{_libdir}/%{name}/coq-tactic
  77 %{_libdir}/%{name}/plugins
  78 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
  79 %attr(755,root,root) %{_libdir}/%{name}/why3-cpulimit
  80
  81 %files examples
  82 %defattr(644,root,root,755)
  83 %{_examplesdir}/%{name}-%{version}