rpms/why
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
why/why.spec

333 lines
11 KiB
RPMSpec
Raw Permalink Blame History

Name: why
Version: 2.23
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-%{version}.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://krakatoa.lri.fr/manual/krakatoa.pdf
# 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
Patch0: gwhy-%{version}.patch
# 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
# It also makes a fix necessary to correctly build the bytecode only
# version of why by building the make_float_model tool correctly in
# this case.
Patch1: why-%{version}-Makefile.in.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
BuildRequires: ocaml-ocamlgraph-devel
BuildRequires: cvc3
ExcludeArch: sparc64 s390 s390x
%if 0%{?fedora} >= 11
# Doesn't seem to build on ppc64 for Fedora >= 11
# bz: 516317
ExcludeArch: ppc64
%endif
# No coq on ppc64 (any Fedora version) at the moment
%ifnarch ppc64
%global has_coq 1
%endif
%global __ocaml_requires_opts -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types
%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.
# No Coq for ppc64 -> certain subpackages can't be built, but main why can be
%if 0%{?has_coq} == 1
%package coq
Group: Applications/Engineering
Summary: Libraries for interfacing Coq with Why
Requires: why = %{version}
BuildRequires: coq
%description coq
This package contains a set of routines that assist in the
manipulation of why Coq-formatted output within Coq.
%endif
%prep
%setup -q
%patch0 -p1
%patch1 -p1
cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .
%build
%global 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
%global opt 0
%endif
# It seems that we should not be creating debuginfo regardless of
# whether we have opt or not, as debuginfo is not particularly useful
# for OCaml programs
# If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
%global debug_package %{nil}
%if ! %{opt}
%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
%else
%global 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} \
%{!?has_coq: COQC=no}
make %{opt_option}
# Remove unnecessary execstack permissions
%if %opt
execstack -c bin/*.opt bin/why-cpulimit
%endif
# Strip binaries (Makefile misses some of them, and don't want to add an extra patch)
strip bin/why-cpulimit
%if %opt
strip bin/*.opt
%endif
%check
%if %opt
%global why bin/why.opt
%else
%global why bin/why.byte
%endif
export WHYLIB=lib
%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} \
%{?has_coq: COQLIB=%{buildroot}%{_datadir}/coq} install
# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
%if 0%{?has_coq} != 1
rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
%endif
# Install desktop icon and menu entry
%global 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
%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
%global why_examples_dir %{why_doc_dir}examples/
%global fix_encoding() dos2unix %1; mv %1 %1.old; \
iconv -f ISO-8859-1 -t UTF-8 < %1.old > %1; rm %1.old \
%{nil}
# 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
%fix_encoding COPYING
cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE %{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
%fix_encoding $f
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
%fix_encoding $f
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
%{why_data_dir}
%exclude %{why_data_dir}/gwhy-icon.png
%{_datadir}/caduceus
%{_datadir}/jessie
# % {_datadir}/krakatoa
%exclude %{_datadir}/jessie/jc.cmo
%if %opt
%exclude %{_datadir}/jessie/jc.cmx
%exclude %{_datadir}/jessie/jc.o
%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
%if 0%{?has_coq} == 1
%files coq
%defattr(-,root,root,-)
%dir %{_datadir}/coq
%dir %{_datadir}/coq/user-contrib
%{_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
%{_datadir}/coq/jessie_why.v*
%doc README.why-coq.Fedora
%endif
%changelog
* Mon Jan 11 2010 Richard W.M. Jones <rjones@gmail.com> - 2.23-2
- Rebuild to fix dependencies.
* Fri Jan 08 2010 Alan Dunn <amdunn@gmail.com> - 2.23-1
- Upgrade to upstream version 2.23
- Move execstack fixing to spec file from patch
- Moved patch descriptions to initial patch declaration as in examples
in Fedora documentation
- New Caduceus, Krakatoa documentation
- Update test result from small test min.mlw
- Added CVC3 interfacing capabilities
- Removed patch for gwhy configuration, as there is a new mechanism for this
* Tue Sep 22 2009 Dennis Gilmore <dennis@ausil.us> - 2.17-5
- Exclude sparc64 s390 s390x there is no ocaml there
* Fri Aug 07 2009 Alan Dunn <amdunn@gmail.com> - 2.17-4
- Removed now irrelevant check for no OCaml in Fedora < 9 (those
distributions are EOL)
- Changed ExcludeArch to proper Fedora versions
- Builds coq subpackage exactly when Coq can be built, thus making
build independent of whether Coq can be built
- define -> global
- Fixed accidental use of in tar ocamlgraph instead of one that is
separately packaged
* Mon Jul 27 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 2.17-1
- Upgrade to version 2.17 (bz: 477790)
- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
- Minor filename change in 2.17 (GPL -> LICENSE)
- Added back Coq .v files to match policy for Coq
- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
- Minor changes to patches to ensure they still work in 2.17
- Corrected package location gwhy-icon.png (should only be in gwhy)
* Tue Aug 5 2008 Alan Dunn <amdunn@gmail.com> 2.14-2.1
- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
* 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.
Reference in a new issue View git blame Copy permalink