why3.spec

   1 Summary:        Software verification platform
   2 Name:           why3
   3 Version:        1.4.0
   4 Release:        1
   5 License:        LGPLv2 with exceptions
   6 Group:          Applications
   7 Source0:        https://gforge.inria.fr/frs/download.php/38425/%{name}-%{version}.tar.gz
   8 # Source0-md5:  9755cedf1edfcacff652149783e18647
   9 URL:            http://why3.lri.fr/
  10 BuildRequires:  camlp5
  11 BuildRequires:  coq >= 8.13
  12 BuildRequires:  ocaml
  13 BuildRequires:  ocaml-findlib-devel
  14 BuildRequires:  ocaml-graph-devel
  15 BuildRequires:  ocaml-lablgtk3-devel
  16 BuildRequires:  ocaml-lablgtk3-gtksourceview-devel
  17 BuildRequires:  ocaml-menhir-devel
  18 BuildRequires:  ocaml-num-devel
  19 BuildRequires:  ocaml-sqlite-devel
  20 BuildRequires:  ocaml-zarith-devel
  21 BuildRequires:  rubber
  22 BuildRequires:  sqlite3-devel
  23 %requires_eq    ocaml-runtime
  24 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  25
  26 %description
  27 Why3 is the next generation of the Why software verification platform.
  28 Why3 clearly separates the purely logical specification part from
  29 generation of verification conditions for programs. It features a rich
  30 library of proof task transformations that can be chained to produce a
  31 suitable input for a large set of theorem provers, including SMT
  32 solvers, TPTP provers, as well as interactive proof assistants.
  33
  34 %package examples
  35 Summary:        Example problems for why3
  36 Group:          Applications
  37 Requires:       %{name} = %{version}-%{release}
  38
  39 %description examples
  40 Example problems for why3.
  41
  42 %prep
  43 %setup -q
  44
  45 %build
  46 %configure \
  47         --enable-doc
  48
  49 %{__make}
  50
  51 %install
  52 rm -rf $RPM_BUILD_ROOT
  53 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
  54
  55 %{__make} install \
  56         DESTDIR=$RPM_BUILD_ROOT
  57
  58 # Move the gtksourceview language file to the right place
  59 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0
  60 %{__mv} $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0/language-specs
  61
  62 cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
  63
  64 %clean
  65 rm -rf $RPM_BUILD_ROOT
  66
  67 %files
  68 %defattr(644,root,root,755)
  69 %doc CHANGES.md README.md
  70 %attr(755,root,root) %{_bindir}/%{name}*
  71 %{_datadir}/%{name}
  72 %{_datadir}/gtksourceview-3.0/language-specs/why3.lang
  73 %{_datadir}/gtksourceview-3.0/language-specs/why3c.lang
  74 %{_datadir}/gtksourceview-3.0/language-specs/why3py.lang
  75 %dir %{_libdir}/%{name}
  76 %{_libdir}/%{name}/coq
  77 %{_libdir}/%{name}/plugins
  78 %dir %{_libdir}/%{name}/commands
  79 %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs
  80 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
  81 %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit
  82 %attr(755,root,root) %{_libdir}/%{name}/why3server
  83
  84 %files examples
  85 %defattr(644,root,root,755)
  86 %{_examplesdir}/%{name}-%{version}