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.
2011-07-11 15:40:19 -06:00 · 2011-07-11 15:40:19 -06:00 · 6fc19ee63f
commit 6fc19ee63f
parent a6d2ac8f9d
6 changed files with 277 additions and 5519 deletions
--- 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
--- a/caduceus.ps
+++ b/caduceus.ps
--- 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
 
--- a/5
+++ b/5
@ -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
--- 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:
--- 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
+%if %{has_pvs}
+BuildRequires:  pvs
 %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
+# 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

-# No Coq for ppc64 -> certain subpackages can't be built, but main why can be
-%if 0%{?has_coq} == 1
+%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:       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
-%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
+%if %{has_pvs}
+make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib
+%else
+make install DESTDIR=%{buildroot} %{opt_option}
+%endif

 # 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
+
+%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@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