why/why.spec

Name:		why
Version:	2.14
Release:	2%{?dist}
Summary:	Why software verification platform

Group:		Applications/Engineering
License:	GPLv2
URL:		http://why.lri.fr/
Source0:	http://why.lri.fr/download/why-2.14.tar.gz
Source1:	README.why-gwhy.Fedora
Source2:	README.why-coq.Fedora
Source3:	README.why
Source4:	gwhy.desktop
Source5:	gwhy-icon.png
Source6:	min.mlw
Source7:	min_why.why.result
Source8:	http://caduceus.lri.fr/manual/caduceus.ps
Source9:	http://gforge.inria.fr/docman/view.php/999/5097/krakatoa.pdf
Patch0:		gwhy-2.14.patch
Patch1:		why-2.14-Makefile.in.patch
Patch2:		why-config.patch
BuildRoot:	%{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildRequires:	ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink, coq

%description
Why is a software verification platform that applies formal proving
tools to annotated programs. It is currently capable of analysis of C
(through the included tool "Caduceus"), Java (through the included
tool "Krakatoa"), and potentially ML programs with some modification
into Why's own ML-like language. Furthermore, Why is capable of
analysis of any program that is mapped onto its own internal
language. It uses a weakest precondition involving calculus to
generate potential theorems necessary for the proof of a program's
correctness. It translates these theorems into formats that can be
used by external proof assistants (without any extra work, Coq, PVS,
HOL Light, Mizar are supported - having one is recommended and Coq is
packaged for Fedora) and automated theorem provers (without any extra
work, Simplify, Alt-Ergo, Yices, Z3, CVC Lite, Zenon are supported and
Zenon is packaged for Fedora) so that these results can be externally
proven, resulting in a proof of program correctness.

%package gwhy
Group:		Applications/Engineering
Summary:	IDE for Why software verification platform
Requires:	why = %{version}, zenity

%description gwhy
Gwhy is an optional graphical user interface for the Why software
coordination platform. It assists in the coordination of dispatching
assertions that need to be proven to different theorem provers by
providing an interface to do this and also supports inspection of why
input files.

%package coq
Group:		Applications/Engineering
Summary:	Libraries for interfacing Coq with Why
Requires:	why = %{version}

%description coq
This package contains a set of routines that assist in the
manipulation of why Coq-formatted output within Coq.

%prep
%setup -q

# The gwhy execution shell script is not particularly informative
# about when bad parameters are passed to it - this patch fixes that
# Upstream has been informed about this issue and a better fix is on
# their todo list, perhaps for 2.15
%patch0

# This patch makes a Fedora-specific fix to eliminate checking for the
# location of Coq - since we're using the coq package, we know where
# it is and their checking causes the rpm building to fail
%patch1

# This patch fixes the creation of a default configuration file in Why
# to use more sensible values for default provers chosen to appear in
# the lefthand GUI window
%patch2

cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .

%build
%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)

# Native ocaml builds do not seem to work on ppc64 (many packages have
# this problem)
%ifarch ppc64
%define opt 0
%endif

# If not building opt, disable the debug info creation as this would otherwise destroy the bytecode executables
# If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
%if ! %{opt}
%define __os_install_post /usr/lib/rpm/brp-compress %{nil}
%define _enable_debug_package 0
%define debug_package %{nil}
%define opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
%else
%define opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif

# We actually want to install library files into a non /usr/lib
# directory as they aren't architecture dependent
./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir}
make %{opt_option}

%check
%if %opt
%define why bin/why.opt
%else
%define why bin/why.byte
%endif
export WHYLIB=lib/why
%why --why --output min min.mlw
unset WHYLIB
diff min_why.why min_why.why.result > /dev/null

%install
rm -rf %{buildroot}
make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} COQLIB=%{buildroot}%{_datadir}/coq install

# Install desktop icon and menu entry

%define why_data_dir %{_datadir}/why
%if %(test -d %{buildroot}%{why_data_dir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{why_data_dir}
%endif
cp gwhy-icon.png %{buildroot}%{why_data_dir}

sed -i -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' gwhy.desktop

desktop-file-install --vendor="fedora"			\
--dir=%{buildroot}%{_datadir}/applications		\
gwhy.desktop

%define why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
%define why_examples_dir %{why_doc_dir}examples/

# Fix up documentation and examples
mkdir -p %{buildroot}%{why_examples_dir}mlw/
mkdir -p %{buildroot}%{why_examples_dir}c/
cp -p doc/manual.ps %{buildroot}%{why_doc_dir}why-manual.ps
cp -p caduceus.ps krakatoa.pdf README.why COPYING GPL %{buildroot}%{why_doc_dir}

# Copy in the example files after converting to proper UTF-8, fix line
# encodings, leaving behind all generated files
cd examples
for d in `find -mindepth 1 -maxdepth 1 -type d`; do
mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
done
for f in `find -regex '.*\(\.mlw\|\.why\)' | egrep -v '_inv|_coq|_why'`; do
dos2unix $f; mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
done

cd ../examples-c
for d in `find -mindepth 1 -maxdepth 1 -type d`; do
mkdir -p %{buildroot}%{why_examples_dir}c/$d
done
for f in `find -regex '.*\.c'`; do
dos2unix $f; mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
cp -p $f %{buildroot}%{why_examples_dir}c/$f
done

%clean
rm -rf %{buildroot}

%files
%defattr(-,root,root,-)
# Binaries
%{_bindir}/*
%exclude %{_bindir}/gwhy*
# Data for programs
%{_datadir}/why
%{_datadir}/caduceus
%{_datadir}/jessie
%{_datadir}/krakatoa
%exclude %{_datadir}/jessie/jc.cmo
%if %opt
%exclude %{_datadir}/jessie/jc.cmx
%endif
# Man page
%{_mandir}/man1/why.1.gz
# Documentation and examples
%{why_doc_dir}
# This last example is really an example only for Coq - only .v files
%exclude %{why_examples_dir}mlw/string-matching/

%files gwhy
%defattr(-,root,root,-)
%{_bindir}/gwhy
%{_bindir}/gwhy-bin
%dir %{why_data_dir}
%doc README.why-gwhy.Fedora
%{why_data_dir}/gwhy-icon.png
%{_datadir}/applications/fedora-gwhy.desktop

%files coq
%defattr(-,root,root,-)
%{_datadir}/coq/user-contrib/Why*
%exclude %{_datadir}/coq/user-contrib/Why*.v
%{_datadir}/coq/user-contrib/caduceus*
%exclude %{_datadir}/coq/user-contrib/caduceus*.v
%{_datadir}/coq/user-contrib/Caduceus.v*
%exclude %{_datadir}/coq/user-contrib/Caduceus.v
%{_datadir}/coq/user-contrib/jessie_why.v*
%exclude %{_datadir}/coq/user-contrib/jessie_why.v
%doc README.why-coq.Fedora

%changelog
* Fri Aug 1 2008 Alan Dunn <amdunn@gmail.com> 2.14-2
- Fixed minor issues in response to package review:
- Inclusion of COPYING, GPL license-related files
- Added config.mll patch to make default config file created nicer
- Changes subpackage dependencies to be fully versioned.
- Makes during build allowed to be noisy (allowed to print).
* Wed Jul 30 2008 Alan Dunn <amdunn@gmail.com> 2.14-1
- Changed to new version of why, removed previous why-cpulimit name
  change, zenon output format patches as the issues were fixed in
  why 2.14.
- Moved doc subpackage back into main package.
- Added example files to documentation subpackage.
- Added check section with test on small why file.
- Reformatted some macro names for greater readability.
* Thu Jul 24 2008 Alan Dunn <amdunn@gmail.com> 2.13-2
- Added several patches: fixed Zenon output, completed fix of rename
  of cpulimit -> why-cpulimit.
* Wed Jul 23 2008 Alan Dunn <amdunn@gmail.com> 2.13-1
- Initial Fedora RPM version.