rpms/why
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
why/why.spec
Jerry James 690799dc3f Patch to work with flocq 2.0.0.
2012-01-11 15:47:54 -07:00

556 lines
19 KiB
RPMSpec
Raw Permalink Blame History

# Whether coq is available
%ifarch %{ocaml_arches}
%global has_coq 1
%else
%global has_coq 0
%endif
# Whether PVS is available
%ifarch %{ix86} x86_64 ppc sparcv9
%global has_pvs 1
%else
%global has_pvs 0
%endif
# What kind of ocaml build to do
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
# Don't create debuginfo; it's not particularly useful for OCaml programs.
%global debug_package %{nil}
Name: why
Version: 2.30
Release: 5%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
License: LPGLv2 with exceptions
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://krakatoa.lri.fr/manual/krakatoa.pdf
Source9: jessie.desktop
Source10: div.pvs
Source11: rem.pvs
Source12: 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-2.26.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-2.30-Makefile.in.patch
# This patch fixes some mildly bitrotted APRON support code.
# Applied upstream.
Patch2: why-apron.patch
# This patch updates the flocq usage for flocq 2.0.0. It will be sent upstream.
Patch3: why-flocq2.patch
BuildRequires: auto-destdir
BuildRequires: cvc3
BuildRequires: desktop-file-utils
BuildRequires: emacs-nox xemacs xemacs-packages-extra
BuildRequires: frama-c-devel
BuildRequires: gappalib-coq
BuildRequires: gtk2-devel
BuildRequires: ocaml
BuildRequires: ocaml-apron-devel
BuildRequires: ocaml-camlp4-devel
BuildRequires: ocaml-lablgtk-devel
BuildRequires: ocaml-ocamldoc
BuildRequires: ocaml-ocamlgraph-devel
%if %{has_coq}
BuildRequires: coq
%endif
%if %{has_pvs}
BuildRequires: pvs
%endif
# Only build on arches that support ocaml
ExclusiveArch: %{ocaml_arches}
# Filter out names that should not be exposed externally
%global __requires_exclude ocaml\\\(((Ast)|(Cc)|(Env)|(Error)|(Loc)|(Logic)|(Logic_decl)|(Misc)|(Parser)|(Project)|(Ptree)|(Types))\\\)
%global __provides_exclude ocaml\\\(((Lexer)|(Lib)|(Loc)|(Output)|(Parser)|(Project)|(Report)|(Xml))\\\)
%description
Why is a software verification platform that applies formal proving
tools to annotated programs. It is currently capable of analysis of C
(through "Frama-C"), 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, and Mizar are supported - having one is
recommended and both Coq and PVS are packaged for Fedora) and automated
theorem provers (without any extra work Simplify, Alt-Ergo, Yices, Z3,
CVC3, and Zenon are supported and Alt-Ergo, CVC3, and Zenon are 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).
%package gwhy
Group: Applications/Engineering
Summary: IDE for Why software verification platform
Requires: %{name}%{?_isa} = %{version}-%{release}, 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 jessie
Group: Applications/Engineering
Summary: Interface between why and frama-c
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: frama-c
%description jessie
The Jessie plugin, an interface between why and frama-c. Invoke it with:
frama-c -jessie FILE.c
%if %{has_coq}
%package coq
Group: Applications/Engineering
Summary: Libraries for interfacing Coq with Why
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: gappalib-coq
%description coq
This package contains a set of routines that assist in the manipulation
of why Coq-formatted output within Coq.
%endif
%if %{has_pvs}
# 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: %{name}%{?_isa} = %{version}-%{release}
Requires: pvs
%description pvs-support
This package provides support definitions so that the Why software
verification platform suite can invoke PVS without licensing issues.
%endif
%package emacs
Summary: Emacs support file for why files
Group: Development/Languages
Requires: %{name} = %{version}-%{release}
Requires: emacs(bin)
BuildArch: noarch
%description emacs
This package contains an Emacs support file for working with why files.
%package emacs-el
Summary: Emacs source file for why support
Group: Development/Languages
Requires: %{name}-emacs = %{version}-%{release}
BuildArch: noarch
%description emacs-el
This package contains the Emacs source file for the Emacs why support.
This package is not needed to use the Emacs support.
%package xemacs
Summary: XEmacs support file for why files
Group: Development/Languages
Requires: %{name} = %{version}-%{release}
Requires: xemacs(bin)
BuildArch: noarch
%description xemacs
This package contains an XEmacs support file for working with why files.
%package xemacs-el
Summary: XEmacs source file for why support
Group: Development/Languages
Requires: %{name}-xemacs = %{version}-%{release}
BuildArch: noarch
%description xemacs-el
This package contains the XEmacs source file for the XEmacs why support.
This package is not needed to use the Emacs support.
%package all
Group: Applications/Engineering
Summary: Complete Why software verification platform suite
Requires: why%{?_isa} = %{version}-%{release}
Requires: why-gwhy%{?_isa} = %{version}-%{release}
Requires: why-jessie%{?_isa} = %{version}-%{release}
%if %{has_coq}
Requires: why-coq%{?_isa} = %{version}-%{release}
%endif
%if %{has_pvs}
Requires: why-pvs-support%{?_isa} = %{version}-%{release}
%endif
Requires: alt-ergo cvc3 gappalib-coq zenon
%description all
This package provides a complete software verification platform suite
based on Why, including various automated and interactive provers.
%prep
%setup -q
%patch0
%patch1
%patch2
%patch3
cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
# Fix missing DESTDIRs in the makefile
sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \
-e 's|$(PVSLIB)/why|$(DESTDIR)$(PVSLIB)/why|' \
-i Makefile.in
%define fix_encoding() \
iconv -f %2 -t %3 %1 > %1.utf8; \
touch -r %1 %1.utf8; \
mv -f %1.utf8 %1;
# Fix encodings
for f in CHANGES COPYING examples/bresenham/bresenham.mlw \
examples/bresenham/bresenham_coq.mlw examples/bresenham/bresenham_inv.mlw \
examples/edit-distance/distance.mlw examples/heapsort/downheap.mlw \
examples/heapsort/heapsort.mlw examples/heapsort/Inftree.v \
examples/kmp/kmp.mlw examples/kmp/Lex.v examples/kmp/Match.v \
examples/kmp/Next.v examples/misc/matrix.why examples/misc/matrix_why.v \
examples/quicksort/partition.mlw examples/quicksort/Partition.v \
examples/quicksort/quicksort.mlw examples/quicksort/Quicksort.v \
examples/sqrt/sqrt.mlw examples/string-matching/Match.v; do
%fix_encoding $f ISO-8859-1 UTF-8
done
# Fix a doubly utf8-encoded file
%fix_encoding examples/sqrt/sqrt_why.v UTF-8 ISO-8859-1
# Fix line endings
for f in examples-c/tutorial/average.c examples-c/tutorial/purse.c \
examples-c/ukkonen/main.c examples-c/ukkonen/ukkonen.c; do
sed "s/\r//" $f > $f.new
touch -r $f $f.new
mv -f $f.new $f
done
# APRON support: add a missing include and a missing rpath
sed -e "s|-I +apron|-I +apron -I +mlgmpidl|" \
-e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
-i configure
%build
%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
# Update the version numbers of external programs
# Also, command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
sed -e 's/versions_ok = \["0\.93"\]/versions_ok = ["0.93";"0.94"]/' \
-e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.31"]/' \
-e 's/versions_ok = \["2.2"\]/versions_ok = ["2.4.1"]/' \
-e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.3pl2"]/' \
-e 's/versions_ok = \["4\.1"\]/versions_ok = ["5.0"]/' \
-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
%if %{has_coq}
%configure --enable-apron --enable-verbosemake
%else
%configure --enable-apron --enable-verbosemake COQC=no
%endif
make %{opt_option}
# Strip binaries (the Makefile misses some of them)
strip bin/why-cpulimit
strip frama-c-plugin/Jessie.cmxs
%if %opt
strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \
bin/why2html.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt
%endif
%install
# Avoid a bug in PVS batch mode when using emacs
make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib \
PVSEMACS=xemacs
# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
%if ! %{has_coq}
rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
%endif
# If no PVS, no .pvs files should be installed
%if ! %{has_pvs}
rm -fr %{buildroot}%{_libdir}/pvs
%endif
# Install desktop icon and menu entry
%global why_data_dir %{_datadir}/why
mkdir -p %{buildroot}%{why_data_dir}
cp -p %{SOURCE5} %{buildroot}%{why_data_dir}
sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE4} > gwhy.desktop
desktop-file-install --vendor="fedora" \
--dir=%{buildroot}%{_datadir}/applications gwhy.desktop
sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE9} > jessie.desktop
desktop-file-install --vendor="fedora" \
--dir=%{buildroot}%{_datadir}/applications jessie.desktop
%if %{has_pvs}
# Get rid of a BUILDROOT reference in a log file (fails QA_CHECK_RPATHS)
sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out
mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/
cp -p %{SOURCE10} %{SOURCE11} %{buildroot}%{_libdir}/pvs/lib/ints/
cp -p %{SOURCE12} %{buildroot}%{_bindir}/
%endif
%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}
%global 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 %{SOURCE8} %{SOURCE3} CHANGES COPYING LICENSE README Version %{buildroot}%{why_doc_dir}
# Copy in the example files, 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
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
cp -p $f %{buildroot}%{why_examples_dir}c/$f
done
# Remove a stray coq file (already installed in the right place)
rm -f %{buildroot}%{_libdir}/coq/jessie_why.v
# Move the Emacs support file to the right places and byte compile it
cd ..
mkdir -p %{buildroot}%{_emacs_sitelispdir}
cp -p lib/emacs/why.el %{buildroot}%{_emacs_sitelispdir}
mkdir -p %{buildroot}%{_xemacs_sitelispdir}
cp -p lib/emacs/why.el %{buildroot}%{_xemacs_sitelispdir}
cd %{buildroot}%{_emacs_sitelispdir}
%{_emacs_bytecompile} why.el
cd %{buildroot}%{_xemacs_sitelispdir}
%{_xemacs_bytecompile} why.el
rm -fr %{buildroot}%{_libdir}/why/emacs
%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.
%files
%{_bindir}/*
%{_libdir}/why/
%{_mandir}/man1/why.1*
%{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*
# why-jessie
%exclude %{_bindir}/jessie
# why-pvs-support:
%exclude %{_bindir}/patch_jessie_pvs
%files gwhy
%doc README.why-gwhy.Fedora
%{_bindir}/gwhy
%{_bindir}/gwhy-bin
%{why_data_dir}/
%{_datadir}/applications/fedora-gwhy.desktop
%files jessie
%{_bindir}/jessie
%{_libdir}/jessie/
%{_libdir}/frama-c/plugins/Jessie.*
%{_datadir}/applications/fedora-jessie.desktop
%if %{has_coq}
%files coq
%doc README.why-coq.Fedora
%{_libdir}/coq/user-contrib/Why/
%endif
%if %{has_pvs}
%files pvs-support
%{_libdir}/pvs/lib/*
%{_bindir}/patch_jessie_pvs
%endif
%files emacs
%{_emacs_sitelispdir}/why.elc
%files emacs-el
%{_emacs_sitelispdir}/why.el
%files xemacs
%{_xemacs_sitelispdir}/why.elc
%files xemacs-el
%{_xemacs_sitelispdir}/why.el
# "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
* Wed Jan 11 2012 Jerry James <loganjerry@gmail.com> - 2.30-5
- Patch to work with flocq 2.0.0
* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 2.30-4
- Rebuild for coq 8.3pl3
* Tue Dec 6 2011 Jerry James <loganjerry@gmail.com> - 2.30-3
- Update alt_ergo and yices "okay" version numbers
* Wed Nov 23 2011 Jerry James <loganjerry@gmail.com> - 2.30-2
- Rebuild with APRON and gappalib-coq support
* Fri Oct 28 2011 Jerry James <loganjerry@gmail.com> - 2.30-1
- New upstream release
* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 2.29-2
- Fix broken conditionals
* Mon Jul 11 2011 Jerry James <loganjerry@gmail.com> - 2.29-1
- New upstream release (fixes FTBFS: bz 715902)
- Remove unnecessary spec file elements (BuildRoot, etc.)
- Update approach to filtering provides and requires
- Add has_pvs analogously to has_coq, and simplify macro usage
- Add (X)Emacs support packages
- New subpackage for the jessie plugin to avoid unowned directories and
permit a direct dependency on frama-c
- Prepare for the eventual availability of APRON
* Thu Apr 14 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.2
- add ppc to excludearch, too. No pvs-sbcl available there
* Wed Apr 13 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.1
- add ppc64 to excludearch, no sbcl available there
* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.28-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.28-1
- Since 2.26 FTBFS, try latest upstream (2.28).
- Rebase Makefile.in patch.
- Fix(?) test result.
- No libdir/frama-c directory is created any more.
* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.26-2
- Bump and rebuild for OCaml 3.12.
* 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