[why] New upstream release.
Jerry James
jjames at fedoraproject.org
Fri Oct 28 17:02:33 UTC 2011
commit 53fa04241292e94763c1ebd93f723ab7cdc8ee82
Author: Jerry James <loganjerry at gmail.com>
Date: Fri Oct 28 11:02:19 2011 -0600
New upstream release.
.gitignore | 3 +-
sources | 5 +-
...Makefile.in.patch => why-2.30-Makefile.in.patch | 6 +-
why.spec | 80 ++++++++++----------
4 files changed, 46 insertions(+), 48 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 02ffd25..3c891f7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,2 @@
-/why-2.29.tar.gz
/krakatoa.pdf
-/caduceus.ps
+/why-2.30.tar.gz
diff --git a/sources b/sources
index 760ff1b..ae20770 100644
--- a/sources
+++ b/sources
@@ -1,3 +1,2 @@
-34d8772de3d68c15a3a12935d90a0d60 krakatoa.pdf
-a7eb00d1f78e59221629604167eb3151 caduceus.ps
-cbb3b109a37f968bea9ffa6e43e3b822 why-2.29.tar.gz
+1e8d6c76e5c3cee018172e981309c68b krakatoa.pdf
+c3f6c5616e32743e883ffb7609f96336 why-2.30.tar.gz
diff --git a/why-2.28-Makefile.in.patch b/why-2.30-Makefile.in.patch
similarity index 82%
rename from why-2.28-Makefile.in.patch
rename to why-2.30-Makefile.in.patch
index 128b4e9..eb43de5 100644
--- a/why-2.28-Makefile.in.patch
+++ b/why-2.30-Makefile.in.patch
@@ -1,6 +1,6 @@
---- Makefile.in.orig 2011-03-02 01:27:41.000000000 -0700
-+++ Makefile.in 2011-07-07 15:41:43.759455717 -0600
-@@ -844,14 +844,9 @@
+--- Makefile.in.orig 2011-10-24 09:21:06.000000000 -0600
++++ Makefile.in 2011-10-25 15:37:54.600278865 -0600
+@@ -782,14 +782,9 @@
cp -f $(V7FILES) $(LIBDIR)/why/coq7
cp -f $(VO7) $(LIBDIR)/why/coq7
install-coq-v8 install-coq-v8.1:
diff --git a/why.spec b/why.spec
index 1c62b01..a312d5f 100644
--- a/why.spec
+++ b/why.spec
@@ -1,5 +1,5 @@
# Whether coq is available
-%ifarch alpha %{arm} %{ix86} ia64 x86_64 ppc sparc sparcv9
+%ifarch %{ocaml_arches}
%global has_coq 1
%else
%global has_coq 0
@@ -19,8 +19,8 @@
%global debug_package %{nil}
Name: why
-Version: 2.29
-Release: 2%{?dist}
+Version: 2.30
+Release: 1%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
@@ -34,12 +34,11 @@ 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
+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.
@@ -53,12 +52,13 @@ Patch0: gwhy-2.26.patch
# 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.28-Makefile.in.patch
+Patch1: why-2.30-Makefile.in.patch
BuildRequires: auto-destdir
BuildRequires: cvc3
BuildRequires: desktop-file-utils
BuildRequires: emacs-nox xemacs-nox
+BuildRequires: flocq
BuildRequires: frama-c-devel
BuildRequires: gtk2-devel
BuildRequires: ocaml
@@ -83,19 +83,19 @@ ExclusiveArch: %{ocaml_arches}
%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, 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.
+(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).
@@ -127,7 +127,7 @@ The Jessie plugin, an interface between why and frama-c. Invoke it with:
Group: Applications/Engineering
Summary: Libraries for interfacing Coq with Why
Requires: %{name}%{?_isa} = %{version}-%{release}
-Requires: coq
+Requires: coq, flocq
%description coq
This package contains a set of routines that assist in the manipulation
@@ -211,7 +211,7 @@ based on Why, including various automated and interactive provers.
%patch0
%patch1
-cp -p %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 %SOURCE11 %SOURCE12 %SOURCE13 ./
+cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
# Fix missing DESTDIRs in the makefile
sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \
@@ -264,9 +264,8 @@ sed -e "s|-I +apron|-I +apron -I +mlgmpidl|" \
# 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\.13\.0"\]/versions_ok = ["0.15.0"]/' \
- -e 's/versions_ok = \["0\.91";.*\]/versions_ok = ["0.93"]/' \
- -e 's/versions_ok = \["1\.0\.17";.*\]/versions_ok = ["1.0.29"]/' \
+sed -e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.30"]/' \
+ -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"/' \
@@ -290,7 +289,9 @@ strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \
%endif
%install
-make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib
+# 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}
@@ -305,11 +306,11 @@ rm -fr %{buildroot}%{_libdir}/pvs
# 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
+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}|' -i jessie.desktop
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE9} > jessie.desktop
desktop-file-install --vendor="fedora" \
--dir=%{buildroot}%{_datadir}/applications jessie.desktop
@@ -317,9 +318,9 @@ desktop-file-install --vendor="fedora" \
# 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 div.pvs rem.pvs %{buildroot}%{_libdir}/pvs/lib/ints/
-cp -p patch_jessie_pvs %{buildroot}%{_bindir}/
+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}
@@ -329,7 +330,7 @@ cp -p patch_jessie_pvs %{buildroot}%{_bindir}/
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 CHANGES COPYING LICENSE README Version %{buildroot}%{why_doc_dir}
+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
@@ -374,7 +375,6 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%files
%{_bindir}/*
-%{_libdir}/caduceus/
%{_libdir}/why/
%{_mandir}/man1/why.1*
%{why_doc_dir}/
@@ -386,8 +386,6 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%exclude %{_bindir}/jessie
# why-pvs-support:
%exclude %{_bindir}/patch_jessie_pvs
-# why-coq:
-%exclude %{_libdir}/caduceus/coq/
%files gwhy
%doc README.why-gwhy.Fedora
@@ -406,7 +404,6 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%files coq
%doc README.why-coq.Fedora
%{_libdir}/coq/user-contrib/Why/
-%{_libdir}/caduceus/coq/
%endif
%if %{has_pvs}
@@ -433,6 +430,9 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%changelog
+* Fri Oct 28 2011 Jerry James <loganjerry at gmail.com> - 2.30-1
+- New upstream release
+
* Thu Jul 14 2011 Jerry James <loganjerry at gmail.com> - 2.29-2
- Fix broken conditionals
More information about the scm-commits
mailing list