rpms/why
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
why/why.spec
David A. Wheeler 31c88ec25f Update to version 2.26
2010-10-11 13:39:21 -04:00

400 lines
15 KiB
RPMSpec
Raw Permalink Blame History

Name: why
Version: 2.26
Release: 1%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
License: GPLv2 and MIT
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
Source10: jessie.desktop
Source11: div.pvs
Source12: rem.pvs
Source13: patch_jessie_pvs
# 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
BuildRequires: ocaml-lablgtk-devel, ocaml-ocamlgraph-devel
BuildRequires: desktop-file-utils, dos2unix, prelink
BuildRequires: frama-c-devel >= 1.5
BuildRequires: auto-destdir
# Emacs is required for PVS to rebuild theories:
BuildRequires: cvc3, pvs-sbcl, emacs
# Specialized dependency generator used because of problems with the
# default RPM OCAML dependency process. Per suggestion of the OCAML group:
%define _use_internal_dependency_generator 0
%define __find_requires /usr/lib/rpm/ocaml-find-requires.sh -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types -i Env -i Misc -i Cil_types -i Db_types -i Lattice_With_Isotropy -i Signature
%define __find_provides /usr/lib/rpm/ocaml-find-provides.sh -i Project
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.
Note: Each user account must be set up by running "why-config" at the
command line (to set up a configuration file). Invoke the Jessie plug-in with:
frama-c -jessie FILE.c
%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
# Why's integration with PVS depends on the NASA Langley PVS Libraries,
# which have no license information. This provides an alternative:
%package pvs-support
Group: Applications/Engineering
Summary: Complete Why software verification platform suite
Requires: why = %{version}
%description pvs-support
This package provides support definitions so that the Why software
verification platform suite can invoke PVS without licensing issues.
%package all
Group: Applications/Engineering
Summary: Complete Why software verification platform suite
Requires: why = %{version}
Requires: why-gwhy = %{version}
%if 0%{?has_coq} == 1
Requires: why-coq = %{version}
%endif
Requires: alt-ergo cvc3 coq pvs-sbcl gappa
%description all
This package provides a complete software verification platform suite
based on Why, including various automated and interactive provers.
%prep
%setup -q
%patch0 -p1
%patch1 -p1
cp -p %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 %SOURCE11 %SOURCE12 %SOURCE13 ./
# Frama-C's makefile does not handle DESTDIR; this lets us override it:
cp -p /usr/share/frama-c/Makefile.dynamic ./frama-c-plugin/
%build
# Native ocaml builds do not work on ppc64 (many packages have this problem)
%ifarch ppc64
%global opt 0
%else
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%endif
%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
# Don't create debuginfo; it's not particularly useful for OCaml programs.
%global debug_package %{nil}
# This option prints the actual make commands so we can see what's
# happening (eg: for debugging the spec file)
%global why_make_options VERBOSEMAKE=yes %{opt_option}
# Remove spurious error and warn if buggy 0.91 is used, per:
# http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-October/002303.html
sed -e 's/versions_ok = \["0\.91"\]/versions_ok = ["0.92.1"]/' -i tools/dpConfig.ml
# Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \
-e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
-i tools/dpConfig.ml
sed -e 's/pvs /pvs-sbcl /' -i configure
# Must disable plug-ins that no longer work, else running will cause warnings.
%configure --disable-security_slicing --disable-aorai PVSC=`which pvs-sbcl` %{!?has_coq: COQC=no}
sed -e 's/\"\/usr\/share\/coq\"/\$(DESTDIR)\/usr\/share\/coq\//' -i Makefile
make %{why_make_options}
# Strip binaries (the Makefile misses some of them)
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
WHYLIB=lib %why --why --output min.why min.mlw
diff -u min.why min_why.why.result # Show differences from correct result.
%install
rm -rf %{buildroot}
mkdir -p %{buildroot}%{_libdir} %{buildroot}%{_bindir} %{buildroot}%{_datadir}
#Edit makefile to use local Makefile.dynamic, and fix local version:
sed -e 's/\$(FRAMAC_SHARE)\/Makefile.dynamic/.\/Makefile.dynamic/' -i ./frama-c-plugin/Makefile
sed -e 's/echo/\# echo/' -i ./frama-c-plugin/Makefile.dynamic
sed -e 's/>>/\# >>/' -i ./frama-c-plugin/Makefile.dynamic
make-redir install DESTDIR=%{buildroot} %{why_make_options} PVSLIB=%{buildroot}%{_libdir}/pvs/lib
sed -e 's!%{buildroot}!!' -i %{buildroot}%{_libdir}/pvs/lib/why/top.out
# 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
mkdir -p %{buildroot}%{why_data_dir}
cp -p gwhy-icon.png %{buildroot}%{why_data_dir}
sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i gwhy.desktop
desktop-file-install --vendor="fedora" \
--dir=%{buildroot}%{_datadir}/applications gwhy.desktop
sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i jessie.desktop
desktop-file-install --vendor="fedora" \
--dir=%{buildroot}%{_datadir}/applications jessie.desktop
mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/
cp -p div.pvs rem.pvs %{buildroot}%{_libdir}/pvs/lib/ints/
cp -p patch_jessie_pvs %{buildroot}%{_bindir}/
%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 -f %1.old ;
# 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\)' | grep -E -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}
%post
echo "ENABLE_JESSIE=yes" >> /usr/share/frama-c/known_plugins.ac
semanage fcontext -a -t textrel_shlib_t '%{_libdir}/frama-c/plugins/Jessie.cmxs'
restorecon '%{_libdir}/frama-c/plugins/Jessie.cmxs'
%postun
sed -e "/ENABLE_JESSIE=yes/d" -i /usr/share/frama-c/known_plugins.ac
%files
%defattr(-,root,root,-)
%{_bindir}/*
%{_libdir}/frama-c/*
%{_libdir}/caduceus/*
%{_libdir}/coq/*
%{_libdir}/jessie/*
%{_libdir}/why/*
%{_libdir}/pvs/lib/why/
%{_datadir}/coq/*
%{_mandir}/man1/why.1.gz
%{why_doc_dir}
# This last example is really an example only for Coq - only .v files
%exclude %{why_examples_dir}mlw/string-matching/
# why-gwhy:
%exclude %{_bindir}/gwhy*
%exclude %{why_data_dir}/gwhy-icon.png
# why-pvs-support:
%exclude %{_bindir}/patch_jessie_pvs
# why-coq:
%exclude %{_datadir}/coq/user-contrib/*
%exclude %{_libdir}/caduceus/coq/
%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
%{_datadir}/applications/fedora-jessie.desktop
%if 0%{?has_coq} == 1
%files coq
%defattr(-,root,root,-)
%{_datadir}/coq/user-contrib/*
%dir %{_libdir}/caduceus/coq/
%doc README.why-coq.Fedora
%endif
%files pvs-support
%defattr(-,root,root,-)
%{_libdir}/pvs/lib/ints/
%{_bindir}/patch_jessie_pvs
# "why-all" is a meta-package; it just depends on other packages, so that
# it's easier to install a useful suite of tools. Thus, it has no files:
%files all
%changelog
* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler@dwheeler.com> - 2.26-1
- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf)
- Integrated with Frama-C and PVS (as pvs-sbcl)
* 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.
# TODO:
# If file $HOME/.gwhyrc does not exist, autorun "why-config".
# Finish packaging/integrating "APRON" (for Inference of annotations)
Reference in a new issue View git blame Copy permalink