[why] New upstream release (fixes FTBFS: bz 715902). Remove unnecessary spec file elements (BuildRoot, etc
Jerry James
jjames at fedoraproject.org
Mon Jul 11 21:41:07 UTC 2011
commit 6fc19ee63f9e247f2ee93451bdff8397d656efdb
Author: Jerry James <loganjerry at gmail.com>
Date: Mon Jul 11 15:40:19 2011 -0600
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.
.gitignore | 6 +-
caduceus.ps | 5358 --------------------------------------------
gwhy-2.26.patch | 4 +-
sources | 5 +-
why-2.28-Makefile.in.patch | 6 +-
why.spec | 417 +++--
6 files changed, 277 insertions(+), 5519 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 2381cf1..02ffd25 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,3 @@
-krakatoa.pdf
-why-2.23.tar.gz
+/why-2.29.tar.gz
/krakatoa.pdf
-/why-2.26.tar.gz
-/why-2.28.tar.gz
+/caduceus.ps
diff --git a/gwhy-2.26.patch b/gwhy-2.26.patch
index 944cd3e..15a2576 100644
--- a/gwhy-2.26.patch
+++ b/gwhy-2.26.patch
@@ -1,5 +1,5 @@
---- why-2.23-old/bin/gwhy.sh 2010-01-04 21:08:50.401993553 -0500
-+++ why-2.23/bin/gwhy.sh 2010-01-05 08:31:05.989807947 -0500
+--- bin/gwhy.sh.orig 2011-03-02 01:27:41.000000000 -0700
++++ bin/gwhy.sh 2011-07-07 15:41:07.232455718 -0600
@@ -1,11 +1,17 @@
#!/bin/sh
diff --git a/sources b/sources
index 77a847d..760ff1b 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,3 @@
-14563361a9427e58115825b4e782d23e krakatoa.pdf
-c1fec836b51a5a10d30da82cfe3bbbb9 why-2.28.tar.gz
+34d8772de3d68c15a3a12935d90a0d60 krakatoa.pdf
+a7eb00d1f78e59221629604167eb3151 caduceus.ps
+cbb3b109a37f968bea9ffa6e43e3b822 why-2.29.tar.gz
diff --git a/why-2.28-Makefile.in.patch b/why-2.28-Makefile.in.patch
index f94625b..128b4e9 100644
--- a/why-2.28-Makefile.in.patch
+++ b/why-2.28-Makefile.in.patch
@@ -1,6 +1,6 @@
---- why-2.28.old/Makefile.in 2010-12-17 20:06:44.000000000 +0000
-+++ why-2.28/Makefile.in 2011-01-21 18:32:55.262077657 +0000
-@@ -843,14 +843,9 @@
+--- 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 @@
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 1e4cbfa..c206caf 100644
--- a/why.spec
+++ b/why.spec
@@ -1,10 +1,30 @@
+# Whether coq is available
+%ifarch alpha %{arm} %{ix86} ia64 x86_64 ppc sparc sparcv9
+%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.28
-Release: 2.2%{?dist}
+Version: 2.29
+Release: 1%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
-License: GPLv2 and MIT
+License: LPGLv2 with exceptions
URL: http://why.lri.fr/
Source0: http://why.lri.fr/download/why-%{version}.tar.gz
Source1: README.why-gwhy.Fedora
@@ -35,185 +55,257 @@ Patch0: gwhy-2.26.patch
# this case.
Patch1: why-2.28-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 ppc ppc64
-%if 0%{?fedora} >= 11
-# Doesn't seem to build on ppc64 for Fedora >= 11
-# bz: 516317
-ExcludeArch: ppc64
+BuildRequires: cvc3
+BuildRequires: desktop-file-utils
+BuildRequires: emacs-nox xemacs-nox
+BuildRequires: frama-c-devel
+BuildRequires: gtk2-devel
+BuildRequires: ocaml
+BuildRequires: ocaml-camlp4-devel
+BuildRequires: ocaml-lablgtk-devel
+BuildRequires: ocaml-ocamldoc
+BuildRequires: ocaml-ocamlgraph-devel
+%if %{has_coq}
+BuildRequires: coq
%endif
-
-# No coq on ppc64 (any Fedora version) at the moment
-%ifnarch ppc64
-%global has_coq 1
+%if %{has_pvs}
+BuildRequires: pvs
%endif
-%global __ocaml_requires_opts -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types
+# 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 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.
+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.
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
-
+command line (to set up a configuration file).
%package gwhy
Group: Applications/Engineering
Summary: IDE for Why software verification platform
-Requires: why = %{version}, zenity
+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
+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
-# No Coq for ppc64 -> certain subpackages can't be built, but main why can be
-%if 0%{?has_coq} == 1
+%if %{has_coq}
%package coq
Group: Applications/Engineering
Summary: Libraries for interfacing Coq with Why
-Requires: why = %{version}
-BuildRequires: coq
+Requires: %{name}%{?_isa} = %{version}-%{release}
+Requires: coq
%description coq
-This package contains a set of routines that assist in the
-manipulation of why Coq-formatted output within 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: why = %{version}
+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 = %{version}
-Requires: why-gwhy = %{version}
-%if 0%{?has_coq} == 1
-Requires: why-coq = %{version}
+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
-Requires: alt-ergo cvc3 coq pvs-sbcl gappa
+%if %{has_pvs}
+Requires: why-pvs-support%{?_isa} = %{version}-%{release}
+%endif
+Requires: alt-ergo cvc3 gappa 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 -p1
-%patch1 -p1
+%patch0
+%patch1
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/
+
+# 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: fix some warnings that -warn-error turns into errors
+sed -i "s/| JCTrange _/| JCTlet _ | JCTrange _/" jc/jc_annot_inference.ml
+
+# 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
-# 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"/' \
+# 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"]/' \
+ -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
-# 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
+sed -e 's/pvs/pvs-sbcl/' -i configure
-
-make %{why_make_options}
+%if %{has_coq}
+%configure --enable-verbosemake
+%else
+%configure --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/*.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
-%check
-%if %opt
-%global why bin/why.opt
+%install
+%if %{has_pvs}
+make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib
%else
-%global why bin/why.byte
+make install DESTDIR=%{buildroot} %{opt_option}
%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
+%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}
@@ -229,26 +321,21 @@ 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 ;
+%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
-%fix_encoding COPYING
-cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE %{buildroot}%{why_doc_dir}
+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}
-# Copy in the example files after converting to proper UTF-8, fix line
-# encodings, leaving behind all generated files
+# 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
- %fix_encoding $f
cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
done
@@ -257,70 +344,90 @@ 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
+# 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
-%clean
-rm -rf %{buildroot}
+# Remove a stray coq file (already installed in the right place)
+rm -f %{buildroot}%{_libdir}/coq/jessie_why.v
-%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'
+# 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
-%postun
-sed -e "/ENABLE_JESSIE=yes/d" -i /usr/share/frama-c/known_plugins.ac
+%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
-%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}
+%{_libdir}/caduceus/
+%{_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*
-%exclude %{why_data_dir}/gwhy-icon.png
+# why-jessie
+%exclude %{_bindir}/jessie
# why-pvs-support:
%exclude %{_bindir}/patch_jessie_pvs
# why-coq:
-%exclude %{_datadir}/coq/user-contrib/*
%exclude %{_libdir}/caduceus/coq/
-
%files gwhy
-%defattr(-,root,root,-)
+%doc README.why-gwhy.Fedora
%{_bindir}/gwhy
%{_bindir}/gwhy-bin
-%dir %{why_data_dir}
-%doc README.why-gwhy.Fedora
-%{why_data_dir}/gwhy-icon.png
+%{why_data_dir}/
%{_datadir}/applications/fedora-gwhy.desktop
-%{_datadir}/applications/fedora-jessie.desktop
+%files jessie
+%{_bindir}/jessie
+%{_libdir}/jessie/
+%{_libdir}/frama-c/plugins/Jessie.*
+%{_datadir}/applications/fedora-jessie.desktop
-%if 0%{?has_coq} == 1
+%if %{has_coq}
%files coq
-%defattr(-,root,root,-)
-%{_datadir}/coq/user-contrib/*
-%dir %{_libdir}/caduceus/coq/
%doc README.why-coq.Fedora
+%{_libdir}/coq/user-contrib/Why/
+%{_libdir}/caduceus/coq/
%endif
+%if %{has_pvs}
%files pvs-support
-%defattr(-,root,root,-)
-%{_libdir}/pvs/lib/ints/
+%{_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:
@@ -328,6 +435,16 @@ sed -e "/ENABLE_JESSIE=yes/d" -i /usr/share/frama-c/known_plugins.ac
%changelog
+* Mon Jul 11 2011 Jerry James <loganjerry at 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 at redhat.com> 2.28-2.2
- add ppc to excludearch, too. No pvs-sbcl available there
More information about the scm-commits
mailing list