why3.spec

   1 Summary:        Software verification platform
   2 Name:           why3
   3 Version:        1.4.0
   4 Release:        3
   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 # same as ocaml-zarith
  25 ExclusiveArch:  %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
  26 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  27
  28 %define         _noautoreq      ocamlx?\\\(Why3\\\)
  29
  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
  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
  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
  57 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
  58
  59 %{__make} install \
  60         DESTDIR=$RPM_BUILD_ROOT
  61
  62 # Move the gtksourceview language file to the right place
  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
  65
  66 cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
  67
  68 %clean
  69 rm -rf $RPM_BUILD_ROOT
  70
  71 %files
  72 %defattr(644,root,root,755)
  73 %doc CHANGES.md README.md
  74 %attr(755,root,root) %{_bindir}/%{name}*
  75 %{_datadir}/%{name}
  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
  79 %dir %{_libdir}/%{name}
  80 %{_libdir}/%{name}/coq
  81 %{_libdir}/%{name}/plugins
  82 %dir %{_libdir}/%{name}/commands
  83 %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs
  84 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
  85 %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit
  86 %attr(755,root,root) %{_libdir}/%{name}/why3server
  87
  88 %files examples
  89 %defattr(644,root,root,755)
  90 %{_examplesdir}/%{name}-%{version}