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 # same as ocaml-zarith
  25 ExclusiveArch:  %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
  26 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  27
  28 %description
  29 Why3 is the next generation of the Why software verification platform.
  30 Why3 clearly separates the purely logical specification part from
  31 generation of verification conditions for programs. It features a rich
  32 library of proof task transformations that can be chained to produce a
  33 suitable input for a large set of theorem provers, including SMT
  34 solvers, TPTP provers, as well as interactive proof assistants.
  35
  36 %package examples
  37 Summary:        Example problems for why3
  38 Group:          Applications
  39 Requires:       %{name} = %{version}-%{release}
  40
  41 %description examples
  42 Example problems for why3.
  43
  44 %prep
  45 %setup -q
  46
  47 %build
  48 %configure \
  49         --enable-doc
  50
  51 %{__make}
  52
  53 %install
  54 rm -rf $RPM_BUILD_ROOT
  55 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
  56
  57 %{__make} install \
  58         DESTDIR=$RPM_BUILD_ROOT
  59
  60 # Move the gtksourceview language file to the right place
  61 install -d $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0
  62 %{__mv} $RPM_BUILD_ROOT%{_datadir}/%{name}/lang $RPM_BUILD_ROOT%{_datadir}/gtksourceview-3.0/language-specs
  63
  64 cp -a examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
  65
  66 %clean
  67 rm -rf $RPM_BUILD_ROOT
  68
  69 %files
  70 %defattr(644,root,root,755)
  71 %doc CHANGES.md README.md
  72 %attr(755,root,root) %{_bindir}/%{name}*
  73 %{_datadir}/%{name}
  74 %{_datadir}/gtksourceview-3.0/language-specs/why3.lang
  75 %{_datadir}/gtksourceview-3.0/language-specs/why3c.lang
  76 %{_datadir}/gtksourceview-3.0/language-specs/why3py.lang
  77 %dir %{_libdir}/%{name}
  78 %{_libdir}/%{name}/coq
  79 %{_libdir}/%{name}/plugins
  80 %dir %{_libdir}/%{name}/commands
  81 %attr(755,root,root) %{_libdir}/%{name}/commands/*.cmxs
  82 %attr(755,root,root) %{_libdir}/%{name}/why3-call-pvs
  83 %attr(755,root,root) %{_libdir}/%{name}/why3cpulimit
  84 %attr(755,root,root) %{_libdir}/%{name}/why3server
  85
  86 %files examples
  87 %defattr(644,root,root,755)
  88 %{_examplesdir}/%{name}-%{version}