Note: This is a beta release of Red Hat Bugzilla 5.0. The data contained within is a snapshot of the live data so any changes you make will not be reflected in the production Bugzilla. Also email is disabled so feel free to test any aspect of the site that you want. File any problems you find or give feedback here.
Bug 456398 - Review Request: why - Why software verification platform
Summary: Review Request: why - Why software verification platform
Keywords:
Status: CLOSED RAWHIDE
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: David A. Wheeler
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2008-07-23 10:27 UTC by Alan Dunn
Modified: 2009-01-25 04:30 UTC (History)
3 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2009-01-25 04:30:29 UTC
dwheeler: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description Alan Dunn 2008-07-23 10:27:47 UTC
Spec URL: http://www.duke.edu/~amd34/why/why.spec
SRPM URL: http://www.duke.edu/~amd34/why/why-2.13-1.fc9.src.rpm
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 ML programs, but in theory 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
automated theorem provers so that these results can be externally
proven, resulting in a proof of program correctness.

Current packaging notes:

- Builds on i386
- Builds in mock
- rpmlint silent
- Meets Fedora packaging criteria (to the best of my knowledge - went through the list)

Comment 1 David A. Wheeler 2008-07-23 15:54:27 UTC
Excellent!!! I've wanted this in Fedora for a while, I'll gladly pick up the review.

Comment 2 David A. Wheeler 2008-07-23 18:36:51 UTC
Must-do's:
* You renamed "cpulimit" to "why-cpulimit", which is sensible enough, but at
least gwhy (and maybe others) still call "cpulimit", so the whole thing fails. 
Quick test:
 sudo yum install -y zenon
 rpmbuild -ba ~/rpmbuild/SPECS/why.spec
 sudo rpm -ivh ~/rpmbuild/RPMS/*/why*.rpm
 cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
 gwhy binary_search.c
 # then click on the "Zenon" column.  Nothing works. Doing:
 strace -f -e trace=process gwhy binary_search.c
 # Note that that it's trying to run "cpulimit" instead. Ooops.
 # After fixing that, re-test.
* Something else is wrong with the installation; even trivial tests of
  caduceus fail.  After building, doing:
  cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
  caduceus max.c
  make -f max.makefile zenon
 Ends in failure. Running:
    strace -v -f -e trace=process make -f max.makefile zenon
 shows that the makefile invokes dp, which in turn tries to call zenon.
 But trying to invoke zenon on the generated file:
   zenon zenon/max_why.znn
 fails with a syntax error.  (I guess it's possible it has a bad bug
 in Zenon.)
* I believe you're missing some "Requires:".  I could "yum erase tcl tk",
  and still install ALL the programs (including gwhy).  rpm can automatically
  deduce a lot of dependencies from library information, but it will miss
  stuff (e.g., stuff invoked via shell/command line).  I was expecting
  gwhy, at least, to have more dependencies.  I think that's a blocker.
* Shouldn't the why-summer-school.tar.gz line include the URL?
* Can you confirm that Fedora has the legal right to redistribute the included
documents?  Fedora doesn't require the right to modify them (though that'd be
nice), but we need to make sure that it's legal to redistributed them.  (Of
course, if we could redistribute the .tex source files, that'd be even better.)

Here are a few suggestions:
* No %check section.   You ought to have SOME test in there, at least as a
'smoke test' to make sure everything can run with a trivial input.  The build's
"bench" subdirectory has useful tests (though you can't run "./bench" directly -
looks like they've changed --type-only and didn't fix the tests).
* You ought to install the examples that come with the distribution, those in
the build directory's "examples/" and "examples-c".  I suggest copying them to
be placed somewhere under /usr/share/doc/..../examples. (you probably want it
further organized than that). The Caduceus web page (http://caduceus.lri.fr/)
points some out.  For the trick to doing this, see:
http://fedoraproject.org/wiki/PackageMaintainers/PackagingTricks#Examples
* /usr/bin/dp is an absurdly short name for /usr/bin, and almost certain to
conflict with SOMETHING.  You might consider renaming that, too.
* I'm slightly surprised that Caduceus, Krakatoa, and Jessie aren't split into
separate packages.  Did you consider splitting them up?  Debian seems to have
done the same thing, so I won't make that a blocker.
* Is there other documentation you can include, e.g., specifically for Caduceus,
Krakatoa, and Jessie?  I see that the makefile can generate the documents, but
that the release doesn't include the source .tex files.
* The description isn't very clear for the unwashed masses, and it should
clearly suggest installing zenon and Coq.  Also: I don't think "why" accepts ML,
really; it accepts the "why" language, which is ML-like but isn't ML.

Other comments:
* License is OSS (GPLv2).  I checked to see if it should be "GPLv2+",
  but the file COPYING makes it clear that this spec file is correct -
  it is GPLv2 alone, not GPLv2+.
* When starting up gwhy, shouldn't it only show the proof tools that are
installed as the default?  I guess that would be additional functionality,
though, so not required for initial packaging.
* In the longer term, the PVS support files should be added too.  But since
there's no Fedora PVS package, that's probably impractical to test.  If PVS is
added to Fedora, then adding those would be a good idea.

I'll try to do a full review later.


Comment 3 David A. Wheeler 2008-07-23 20:19:01 UTC
Looks like depending on the name "/usr/bin/dp" is all over their generated
makefiles.  That's terrible, but hardly your fault.  Probably it's best to go
ahead and accept this terribly short name as-is, since users would have trouble
if you renamed it.... their files wouldn't work.


Comment 4 Alan Dunn 2008-07-24 20:11:44 UTC
(In reply to comment #2)

I'm addressing these as I write, but I thought it'd be good to comment on how 
they're going/what I think about them.

> Must-do's:
> * You renamed "cpulimit" to "why-cpulimit", which is sensible enough, but at
> least gwhy (and maybe others) still call "cpulimit", so the whole thing 
fails. 
> Quick test:
>  sudo yum install -y zenon
>  rpmbuild -ba ~/rpmbuild/SPECS/why.spec
>  sudo rpm -ivh ~/rpmbuild/RPMS/*/why*.rpm
>  cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
>  gwhy binary_search.c
>  # then click on the "Zenon" column.  Nothing works. Doing:
>  strace -f -e trace=process gwhy binary_search.c
>  # Note that that it's trying to run "cpulimit" instead. Ooops.
>  # After fixing that, re-test.

Whoops, that's definitely my fault. Fixed in the next version (another patch).

> * Something else is wrong with the installation; even trivial tests of
>   caduceus fail.  After building, doing:
>   cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
>   caduceus max.c
>   make -f max.makefile zenon
>  Ends in failure. Running:
>     strace -v -f -e trace=process make -f max.makefile zenon
>  shows that the makefile invokes dp, which in turn tries to call zenon.
>  But trying to invoke zenon on the generated file:
>    zenon zenon/max_why.znn
>  fails with a syntax error.  (I guess it's possible it has a bad bug
>  in Zenon.)

I figured out that Why's Zenon output is wrong (it changed
between Zenon versions and remained undetected due to the
complete lack of Zenon documentation). I contacted upstream, and
they wrote a patch for me this morning. The change will be added
to the next version of Why.

> * I believe you're missing some "Requires:".  I could "yum erase tcl tk",
>   and still install ALL the programs (including gwhy).  rpm can 
automatically
>   deduce a lot of dependencies from library information, but it will miss
>   stuff (e.g., stuff invoked via shell/command line).  I was expecting
>   gwhy, at least, to have more dependencies.  I think that's a blocker.

I'll look at this.

> * Shouldn't the why-summer-school.tar.gz line include the URL?

No, because I created that file (a few PDFs packaged up).

> * Can you confirm that Fedora has the legal right to redistribute the 
included
> documents?  Fedora doesn't require the right to modify them (though that'd 
be
> nice), but we need to make sure that it's legal to redistributed them.  (Of
> course, if we could redistribute the .tex source files, that'd be even 
better.)

I'll ask upstream.

> Here are a few suggestions:
> * No %check section.   You ought to have SOME test in there, at least as a
> 'smoke test' to make sure everything can run with a trivial input.  The 
build's
> "bench" subdirectory has useful tests (though you can't run "./bench" 
directly -
> looks like they've changed --type-only and didn't fix the tests).

Right, I originally wanted to run their tests, but they didn't
work. I did make my own (exceptionally brief) test, but I haven't
included it yet - I will.

> * You ought to install the examples that come with the distribution, those 
in
> the build directory's "examples/" and "examples-c".  I suggest copying them 
to
> be placed somewhere under /usr/share/doc/..../examples. (you probably want 
it
> further organized than that). The Caduceus web page 
(http://caduceus.lri.fr/)
> points some out.  For the trick to doing this, see:
> http://fedoraproject.org/wiki/PackageMaintainers/PackagingTricks#Examples

The example Makefiles are odd: the library files need to have
already been installed in the right places before the examples
can be compiled. Thus I can't put both in the build section, and
it doesn't seem right to put this in the install section...

> * /usr/bin/dp is an absurdly short name for /usr/bin, and almost certain to
> conflict with SOMETHING.  You might consider renaming that, too.

Changing dp's name would require patches for the following files:

Makefile.in
examples/Makefile.common
bench/java/bench

but I believe that's it (however, I could be introducing errors
here... again, maybe I'll suggest this change to upstream instead
who would better know how to fix it)

> * I'm slightly surprised that Caduceus, Krakatoa, and Jessie aren't split 
into
> separate packages.  Did you consider splitting them up?  Debian seems to 
have
> done the same thing, so I won't make that a blocker.

I wasn't quite sure, and Debian didn't, so I didn't.

> * Is there other documentation you can include, e.g., specifically for 
Caduceus,
> Krakatoa, and Jessie?  I see that the makefile can generate the documents, 
but
> that the release doesn't include the source .tex files.

I'll check on that.

> * The description isn't very clear for the unwashed masses, and it should
> clearly suggest installing zenon and Coq.  Also: I don't think "why" accepts 
ML,
> really; it accepts the "why" language, which is ML-like but isn't ML.

True - I'll clarify that.

Comment 5 Alan Dunn 2008-07-24 21:18:26 UTC
> * I believe you're missing some "Requires:".  I could "yum erase tcl tk",
>   and still install ALL the programs (including gwhy).  rpm can 
automatically
>   deduce a lot of dependencies from library information, but it will miss
>   stuff (e.g., stuff invoked via shell/command line).  I was expecting
>   gwhy, at least, to have more dependencies.  I think that's a blocker.

gwhy has a lot of requires (as automatically determined by the RPM build 
system):

/bin/sh
libatk-1.0.so.0
libc.so.6
libc.so.6(GLIBC_2.0)
libc.so.6(GLIBC_2.1)
libc.so.6(GLIBC_2.1.2)
libc.so.6(GLIBC_2.2)
libc.so.6(GLIBC_2.3)
libc.so.6(GLIBC_2.3.4)
libc.so.6(GLIBC_2.4)
libcairo.so.2
libdl.so.2
libdl.so.2(GLIBC_2.0)
libdl.so.2(GLIBC_2.1)
libgdk-x11-2.0.so.0
libgdk_pixbuf-2.0.so.0
libglib-2.0.so.0
libgmodule-2.0.so.0
libgobject-2.0.so.0
libgtk-x11-2.0.so.0
libm.so.6
libm.so.6(GLIBC_2.0)
libpango-1.0.so.0
libpangocairo-1.0.so.0
libpthread.so.0
libpthread.so.0(GLIBC_2.0)
libpthread.so.0(GLIBC_2.1)
libpthread.so.0(GLIBC_2.2)
libpthread.so.0(GLIBC_2.3.2)
rpmlib(CompressedFileNames) <= 3.0.4-1
rpmlib(PayloadFilesHavePrefix) <= 4.0-1
rtld(GNU_HASH)
why
zenity

What other ones would it have? There are no packages "tcl" or "tk"... it 
certainly doesn't require "tcllib" and "tklib". Furthermore, gwhy really 
depends on gtk, not tk (which it does indeed appropriately require as above). 
I'm pretty sure rpmbuild indeed saw that gwhy was just a shell script that 
calls gwhy-bin (since running find-requires on just gwhy produces /bin/sh). 
Was there something else you had in mind?

Comment 6 David A. Wheeler 2008-07-25 22:13:37 UTC
(In reply to comment #4)

> I figured out that Why's Zenon output is wrong (it changed
> between Zenon versions and remained undetected due to the
> complete lack of Zenon documentation). I contacted upstream, and
> they wrote a patch for me this morning. The change will be added
> to the next version of Why.

That is absolutely fantastic.  Thanks for tracking that down.
Since I'm the Fedora packager for Zenon, I definitely want to make sure that
the two can work together :-).

Also: Don't change the name of "dp" at the moment.
Anybody who has pre-existing data will have generated makefiles
that call "dp", and changing the name will make their existing
data not work.  Instead, could you talk with upstream and
try to convince them to use a longer name, one less likely
to conflict with existing packages?  If _upstream_ makes the
change, then they make the change a lot more graceful than if you
just abruptly do it here.

(In reply to comment #5)

This may not be a problem after all.

When I tried to re-build this package, I had to install other things that in
turn pulled in tcl/tk... but when I "rpm -e tcl tk", I could still install this
package.  But in retrospect, I suspect that the issue is that you depended on
something for building that wants tcl/tk merely to enable certain compile-time
options.  As long as "Why" doesn't require tcl/tk, then clearly it shouldn't
include it as a "Requires:".

Okay, never mind, looks like it's not a real issue.



Comment 7 David A. Wheeler 2008-07-25 22:19:55 UTC
(in reply to comment #4)

>> * You ought to install the examples...

> The example Makefiles are odd: the library files need to have
already been installed in the right places before the examples
can be compiled. Thus I can't put both in the build section, and
it doesn't seem right to put this in the install section...

Why not?  All you're doing is taking the examples, as included in
the distribution, and installing them.  I think people could
learn a LOT from the examples, so they should be included in the
final package.  They aren't large, so I don't think you need to
put them in a separate sub-package.


Comment 8 Alan Dunn 2008-07-30 18:24:19 UTC
I have created a new version to address your comments. It is based off of
why-2.14, a new release which incorporates some of the issues I mentioned here
that I reported to upstream.

SRPM: http://www.duke.edu/~amd34/why/why-2.14-1.fc9.src.rpm
SPEC: http://www.duke.edu/~amd34/why/why.spec

(In reply to comment #2)
> Must-do's:
> * You renamed "cpulimit" to "why-cpulimit", which is sensible enough, but at
> least gwhy (and maybe others) still call "cpulimit", so the whole thing fails. 
> Quick test:
>  sudo yum install -y zenon
>  rpmbuild -ba ~/rpmbuild/SPECS/why.spec
>  sudo rpm -ivh ~/rpmbuild/RPMS/*/why*.rpm
>  cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
>  gwhy binary_search.c
>  # then click on the "Zenon" column.  Nothing works. Doing:
>  strace -f -e trace=process gwhy binary_search.c
>  # Note that that it's trying to run "cpulimit" instead. Ooops.
>  # After fixing that, re-test.

dp, cpulimit were renamed to why-dp, why-cpulimit in 2.14. With gwhy I can
successfully prove swap0.mlw from the examples. (Note: other files may time
out... this is a very hit or miss thing. There are more issues on this note that
I have been discussing with upstream.)

> * Something else is wrong with the installation; even trivial tests of
>   caduceus fail.  After building, doing:
>   cd ~/rpmbuild/BUILD/why-2.13/examples-c/tutorial
>   caduceus max.c
>   make -f max.makefile zenon
>  Ends in failure. Running:
>     strace -v -f -e trace=process make -f max.makefile zenon
>  shows that the makefile invokes dp, which in turn tries to call zenon.
>  But trying to invoke zenon on the generated file:
>    zenon zenon/max_why.znn
>  fails with a syntax error.  (I guess it's possible it has a bad bug
>  in Zenon.)

The Zenon syntax error (their file format changed and upstream was not aware) is
fixed in 2.14.

> * Shouldn't the why-summer-school.tar.gz line include the URL?
> * Can you confirm that Fedora has the legal right to redistribute the included
> documents?  Fedora doesn't require the right to modify them (though that'd be
> nice), but we need to make sure that it's legal to redistributed them.  (Of
> course, if we could redistribute the .tex source files, that'd be even better.)

I actually decided the user would be better off visiting the why manual page for
supplementary documentation besides the current manual - it's in a moderate
state of flux anyway. (As a result, I removed the summer school tar and informed
the user about the location of the website in README.why.)

> Here are a few suggestions:
> * No %check section.   You ought to have SOME test in there, at least as a
> 'smoke test' to make sure everything can run with a trivial input.  The build's
> "bench" subdirectory has useful tests (though you can't run "./bench" directly -
> looks like they've changed --type-only and didn't fix the tests).

A test is now performed: why is run on a file and its output is compared to a
known result.

> * You ought to install the examples that come with the distribution, those in
> the build directory's "examples/" and "examples-c".  I suggest copying them to
> be placed somewhere under /usr/share/doc/..../examples. (you probably want it
> further organized than that). The Caduceus web page (http://caduceus.lri.fr/)
> points some out.  For the trick to doing this, see:
> http://fedoraproject.org/wiki/PackageMaintainers/PackagingTricks#Examples

Done. Appears in %{_defaultdocdir}/examples/(c or mlw)/<example name>

> * I'm slightly surprised that Caduceus, Krakatoa, and Jessie aren't split into
> separate packages.  Did you consider splitting them up?  Debian seems to have
> done the same thing, so I won't make that a blocker.

I'm still putting these together for now.

> * Is there other documentation you can include, e.g., specifically for Caduceus,
> Krakatoa, and Jessie?  I see that the makefile can generate the documents, but
> that the release doesn't include the source .tex files.

Caduceus and Krakatoa manuals are now included.

> * The description isn't very clear for the unwashed masses, and it should
> clearly suggest installing zenon and Coq.  Also: I don't think "why" accepts ML,
> really; it accepts the "why" language, which is ML-like but isn't ML.

Description was modified.

Comment 9 David A. Wheeler 2008-07-30 22:05:55 UTC
Great, I've started reviewing the package right now.  Bonus points to you for
getting "dp" renamed _upstream_, that is a credit to both you and upstream.  I
see that they fixed the Zenon syntax bug, and at lightening speed - great! The
latest version of Zenon (my package) now includes two man pages, including a man
page on its input syntax.


Comment 10 David A. Wheeler 2008-07-31 03:26:30 UTC
Okay, I've looked this over, installed on my own system and tested it, etc.
It's generally quite good, but there are a few issues... but I think they'll be
really easy to fix.

* rpmls of each binary package looks fine (permissions reasonable)

- MUST: rpmlint must be run on every package. The output should be posted in the
review.
Ok. No errors, and the warning is a well-known one
that is the fault of the ocaml compiler.  See:
 https://bugzilla.redhat.com/show_bug.cgi?id=450551
 http://caml.inria.fr/mantis/view.php?id=4564
 http://groups.google.com/group/fa.caml/browse_thread/thread/2d247a192eb92826

 But you could do better; apply "execstack -c" to ELF files in /usr/bin,
 and the programs will run without an executable stack.
 That's a better idea; OCaml doesn't actually require an executable stack,
 and the noexec stack will protect the low-level C routines it calls.

$ rpmlint SPECS/why.spec SRPMS/why-2.14-1.fc9.src.rpm \
          RPMS/i386/why-2.14-1.fc9.i386.rpm 
why.i386: W: executable-stack /usr/bin/why-stat
why.i386: W: executable-stack /usr/bin/why2html
why.i386: W: executable-stack /usr/bin/why-dp
why.i386: W: executable-stack /usr/bin/caduceus
why.i386: W: executable-stack /usr/bin/rv_merge
why.i386: W: executable-stack /usr/bin/why
why.i386: W: executable-stack /usr/bin/jessie
why.i386: W: executable-stack /usr/bin/simplify2why
why.i386: W: executable-stack /usr/bin/why-obfuscator
why.i386: W: executable-stack /usr/bin/krakatoa
2 packages and 1 specfiles checked; 0 errors, 10 warnings.

- MUST: The package must be named according to the Package Naming Guidelines
OK.

- MUST: The spec file name must match the base package %{name}, in the format
%{name}.spec unless your package has an exemption on Package Naming Guidelines.
OK

- MUST: The package must meet the Packaging Guidelines.
OK (I didn't see any errors)

- MUST: The package must be licensed with a Fedora approved license and meet the
Licensing Guidelines.
OK (GPLv2)

- MUST: The License field in the package spec file must match the actual license.
Yes; README, INSTALL, and COPYING all quite explicit that it is GPLv2.

- MUST: If (and only if) the source package includes the text of the license(s)
in its own file, then that file, containing the text of the license(s) for the
package must be included in %doc.

FAIL.  At _least_ install file "COPYING" in %doc, and go ahead and include "GPL"
too.

- MUST: The spec file must be written in American English.
OK

- MUST: The spec file for the package MUST be legible. If the reviewer is unable
to read the spec file, it will be impossible to perform a review. Fedora is not
the place for entries into the Obfuscated Code Contest (http://www.ioccc.org/).
OK

- MUST: The sources used to build the package must match the upstream source, as
provided in the spec URL. Reviewers should use md5sum for this task. If no
upstream URL can be specified for this package, please see the Source URL
Guidelines for how to deal with this.
OK

- MUST: The package must successfully compile and build into binary rpms on at
least one supported architecture.
OK

- MUST: If the package does not successfully compile, build or work on an
architecture, then those architectures should be listed in the spec in
ExcludeArch. Each architecture listed in ExcludeArch needs to have a bug filed
in bugzilla, describing the reason that the package does not compile/build/work
on that architecture. The bug number should then be placed in a comment, next to
the corresponding ExcludeArch line. New packages will not have bugzilla entries
during the review process, so they should put this description in the comment
until the package is approved, then file the bugzilla entry, and replace the
long explanation with the bug number. The bug should be marked as blocking one
(or more) of the following bugs to simplify tracking such issues:
FE-ExcludeArch-x86 , FE-ExcludeArch-x64 , FE-ExcludeArch-ppc , FE-ExcludeArch-ppc64
OK

- MUST: All build dependencies must be listed in BuildRequires, except for any
that are listed in the [wiki:Self:Packaging/Guidelines#Exceptions exceptions
section of Packaging Guidelines] ; inclusion of those as BuildRequires is
optional. Apply common sense.
OK (builds in mock)

- MUST: The spec file MUST handle locales properly. This is done by using the
%find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.
OK (No locale issue).

- MUST: Every binary RPM package which stores shared library files (not just
symlinks) in any of the dynamic linker's default paths, must call ldconfig in
%post and %postun....
OK (N/A)

- MUST: If the package is designed to be relocatable...
OK (N/A)

- MUST: A package must own all directories that it creates. If it does not
create a directory that it uses, then it should require a package which does
create that directory. Refer to the Guidelines for examples.
OK

- MUST: A package must not contain any duplicate files in the %files listing.
OK

- MUST: Permissions on files must be set properly. Executables should be set
with executable permissions, for example. Every %files section must include a
%defattr(...) line.
OK.  I checked the permissions on the binary RPMs using rpmls, looks okay.

- MUST: Each package must have a %clean section, which contains rm -rf
%{buildroot} ([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or
$RPM_BUILD_ROOT] ).
OK

- MUST: Each package must consistently use macros, as described in the
[wiki:Self:Packaging/Guidelines#macros macros section of Packaging Guidelines].
OK

- MUST: The package must contain code, or permissable content. This is described
in detail in the [wiki:Self:Packaging/Guidelines#CodeVsContent code vs. content
section of Packaging Guidelines] .
OK

- MUST: Large documentation files should go in a -doc subpackage. (The
definition of large is left up to the packager's best judgement, but is not
restricted to size. Large can refer to either size or quantity)
OK (N/A)

- MUST: If a package includes something as %doc, it must not affect the runtime
of the application. To summarize: If it is in %doc, the program must run
properly if it is not present.
OK

- MUST: Header files must be in a -devel package.
OK (N/A)

- MUST: Static libraries must be in a -static package.
OK (N/A)

- MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for
directory ownership and usability).
OK (N/A)

- MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1),
then library files that end in .so (without suffix) must go in a -devel package.
OK (N/A)

- MUST: In the vast majority of cases, devel packages must require the base
package using a fully versioned dependency: Requires: %{name} =
%{version}-%{release}
OK (N/A)

- MUST: Packages must NOT contain any .la libtool archives, these should be
removed in the spec.
OK (N/A)

- MUST: Packages containing GUI applications must include a %{name}.desktop
file, and that file must be properly installed with desktop-file-install in the
%install section.
OK (Verified on desktop)

- MUST: Packages must not own files or directories already owned by other
packages. The rule of thumb here is that the first package to be installed
should own the files or directories that other packages may rely upon. This
means, for example, that no package in Fedora should ever share ownership with
any of the files or directories owned by the filesystem or man package. If you
feel that you have a good reason to own a file or directory that another package
owns, then please present that at package review time.
OK.  I don't know how to check that automatically, but a look using rpmls at the
binary files looks okay.

- MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot}
([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or $RPM_BUILD_ROOT] ).
See [wiki:Self:Packaging/Guidelines#PreppingBuildRootForInstall Prepping
BuildRoot For %install] for details.
OK

- MUST: All filenames in rpm packages must be valid UTF-8.
OK.


Serious problems:
* gwhy fails if the .c file isn't in the current directory (home directory if
invoked from the GUI).
* In the Zenity patch, use --file-selection not --entry to get the filename.
That way, people can use a GUI to traverse the directory structure and click on
the right file.

Strongly recommend fixing:
* apply "execstack -c" to ELF files in /usr/bin, as noted above. (But only if
they're ELF, don't do that to bytecode).  That will enable the exec-stack
protection, there's no reason it should be disabled.
* In the description, change "Furthermore, in theory," to just "Furthermore". 
To a lot of people, "in theory" means "not really". Since they've demonstrated
the truth of the claim for 2 rather different languages, I think they've proved
that claim.
* By default gwhy gives a HUGE list of potential provers, even when they aren't
installed.  That's a big pain - you want beginning users to have a reasonable
view when they start!! In the long term, I think upstream should modify gwhy so
that at start-up it detects which provers exist, and only shows the ones that
are installed.  For the short term, can you modify the defaults so that by
default, if the user hasn't made any selections, only Zenon, Ergo, and CVC3 are
shown?

Other suggestions:
* Simplify this comment:
 # Native ocaml builds do not seem to work on ppc64 (not the first
 # package for which this has been true)
 to something shorter like this:
 # Native ocaml builds don't work on ppc64 (many packages have this problem)

* I think you should modify the %files list to use wildcards and %exclude,
instead of (for example) listing every file in /usr/bin.  It would simplify the
%files list greatly.  It would also make updates much easier; if a future
version of the package installs some new files (e.g., in /usr/bin), the spec
file would be more likely to "just work" if it used wildcards.  E.G., I suggest
something like this:
%files
%{_bindir}/*
%exclude %{_bindir}/gwhy*
...
 You must _not_ say "%{bindir}/" (that tries to grab /usr/bin itself), but
%{bindir}/* is fine... and in this case, I think it's preferable.


Zenon doesn't manage to solve many of them, but it at least manages some,
so clearly the basic bug in invoking Zenon has been fixed.


Comment 11 David A. Wheeler 2008-07-31 03:30:09 UTC
Most of the SHOULDs don't apply, but I think this one does:
- SHOULD: Usually, subpackages other than devel should require the base package
using a fully versioned dependency.

The subpackages aren't fully versioned.  Is there a reason for that?


Comment 12 Alan Dunn 2008-08-02 03:24:23 UTC
I made a new version to incorporate your suggested changes:

SRPM: http://www.duke.edu/~amd34/why/why-2.14-2.fc9.src.rpm
SPEC: http://www.duke.edu/~amd34/why/why.spec

(In reply to comment #10)
> Okay, I've looked this over, installed on my own system and tested it, etc.
> It's generally quite good, but there are a few issues... but I think they'll be
> really easy to fix.
> 
> * rpmls of each binary package looks fine (permissions reasonable)
> 
> - MUST: rpmlint must be run on every package. The output should be posted in the
> review.
> Ok. No errors, and the warning is a well-known one
> that is the fault of the ocaml compiler.  See:
>  https://bugzilla.redhat.com/show_bug.cgi?id=450551
>  http://caml.inria.fr/mantis/view.php?id=4564
>  http://groups.google.com/group/fa.caml/browse_thread/thread/2d247a192eb92826
> 
>  But you could do better; apply "execstack -c" to ELF files in /usr/bin,
>  and the programs will run without an executable stack.
>  That's a better idea; OCaml doesn't actually require an executable stack,
>  and the noexec stack will protect the low-level C routines it calls.
> 
> $ rpmlint SPECS/why.spec SRPMS/why-2.14-1.fc9.src.rpm \
>           RPMS/i386/why-2.14-1.fc9.i386.rpm 
> why.i386: W: executable-stack /usr/bin/why-stat
> why.i386: W: executable-stack /usr/bin/why2html
> why.i386: W: executable-stack /usr/bin/why-dp
> why.i386: W: executable-stack /usr/bin/caduceus
> why.i386: W: executable-stack /usr/bin/rv_merge
> why.i386: W: executable-stack /usr/bin/why
> why.i386: W: executable-stack /usr/bin/jessie
> why.i386: W: executable-stack /usr/bin/simplify2why
> why.i386: W: executable-stack /usr/bin/why-obfuscator
> why.i386: W: executable-stack /usr/bin/krakatoa
> 2 packages and 1 specfiles checked; 0 errors, 10 warnings.

Fixed - turns out that (as I mentioned to you separately) I was not seeing these
warnings due to an old version of rpmlint (oops). I took your suggestion -
running execstack -c on all (native code) binaries.

> - MUST: The package must be named according to the Package Naming Guidelines
> OK.
> 
> - MUST: The spec file name must match the base package %{name}, in the format
> %{name}.spec unless your package has an exemption on Package Naming Guidelines.
> OK
> 
> - MUST: The package must meet the Packaging Guidelines.
> OK (I didn't see any errors)
> 
> - MUST: The package must be licensed with a Fedora approved license and meet the
> Licensing Guidelines.
> OK (GPLv2)
> 
> - MUST: The License field in the package spec file must match the actual license.
> Yes; README, INSTALL, and COPYING all quite explicit that it is GPLv2.
> 
> - MUST: If (and only if) the source package includes the text of the license(s)
> in its own file, then that file, containing the text of the license(s) for the
> package must be included in %doc.
> 
> FAIL.  At _least_ install file "COPYING" in %doc, and go ahead and include "GPL"
> too.

Fixed.

> - MUST: The spec file must be written in American English.
> OK
> 
> - MUST: The spec file for the package MUST be legible. If the reviewer is unable
> to read the spec file, it will be impossible to perform a review. Fedora is not
> the place for entries into the Obfuscated Code Contest (http://www.ioccc.org/).
> OK
> 
> - MUST: The sources used to build the package must match the upstream source, as
> provided in the spec URL. Reviewers should use md5sum for this task. If no
> upstream URL can be specified for this package, please see the Source URL
> Guidelines for how to deal with this.
> OK
> 
> - MUST: The package must successfully compile and build into binary rpms on at
> least one supported architecture.
> OK
> 
> - MUST: If the package does not successfully compile, build or work on an
> architecture, then those architectures should be listed in the spec in
> ExcludeArch. Each architecture listed in ExcludeArch needs to have a bug filed
> in bugzilla, describing the reason that the package does not compile/build/work
> on that architecture. The bug number should then be placed in a comment, next to
> the corresponding ExcludeArch line. New packages will not have bugzilla entries
> during the review process, so they should put this description in the comment
> until the package is approved, then file the bugzilla entry, and replace the
> long explanation with the bug number. The bug should be marked as blocking one
> (or more) of the following bugs to simplify tracking such issues:
> FE-ExcludeArch-x86 , FE-ExcludeArch-x64 , FE-ExcludeArch-ppc ,
FE-ExcludeArch-ppc64
> OK
> 
> - MUST: All build dependencies must be listed in BuildRequires, except for any
> that are listed in the [wiki:Self:Packaging/Guidelines#Exceptions exceptions
> section of Packaging Guidelines] ; inclusion of those as BuildRequires is
> optional. Apply common sense.
> OK (builds in mock)

(Still builds in mock.)

> - MUST: The spec file MUST handle locales properly. This is done by using the
> %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.
> OK (No locale issue).
> 
> - MUST: Every binary RPM package which stores shared library files (not just
> symlinks) in any of the dynamic linker's default paths, must call ldconfig in
> %post and %postun....
> OK (N/A)
> 
> - MUST: If the package is designed to be relocatable...
> OK (N/A)
> 
> - MUST: A package must own all directories that it creates. If it does not
> create a directory that it uses, then it should require a package which does
> create that directory. Refer to the Guidelines for examples.
> OK
> 
> - MUST: A package must not contain any duplicate files in the %files listing.
> OK
> 
> - MUST: Permissions on files must be set properly. Executables should be set
> with executable permissions, for example. Every %files section must include a
> %defattr(...) line.
> OK.  I checked the permissions on the binary RPMs using rpmls, looks okay.
> 
> - MUST: Each package must have a %clean section, which contains rm -rf
> %{buildroot} ([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or
> $RPM_BUILD_ROOT] ).
> OK
> 
> - MUST: Each package must consistently use macros, as described in the
> [wiki:Self:Packaging/Guidelines#macros macros section of Packaging Guidelines].
> OK
> 
> - MUST: The package must contain code, or permissable content. This is described
> in detail in the [wiki:Self:Packaging/Guidelines#CodeVsContent code vs. content
> section of Packaging Guidelines] .
> OK
> 
> - MUST: Large documentation files should go in a -doc subpackage. (The
> definition of large is left up to the packager's best judgement, but is not
> restricted to size. Large can refer to either size or quantity)
> OK (N/A)
> 
> - MUST: If a package includes something as %doc, it must not affect the runtime
> of the application. To summarize: If it is in %doc, the program must run
> properly if it is not present.
> OK
> 
> - MUST: Header files must be in a -devel package.
> OK (N/A)
> 
> - MUST: Static libraries must be in a -static package.
> OK (N/A)
> 
> - MUST: Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig' (for
> directory ownership and usability).
> OK (N/A)
> 
> - MUST: If a package contains library files with a suffix (e.g. libfoo.so.1.1),
> then library files that end in .so (without suffix) must go in a -devel package.
> OK (N/A)
> 
> - MUST: In the vast majority of cases, devel packages must require the base
> package using a fully versioned dependency: Requires: %{name} =
> %{version}-%{release}
> OK (N/A)
> 
> - MUST: Packages must NOT contain any .la libtool archives, these should be
> removed in the spec.
> OK (N/A)
> 
> - MUST: Packages containing GUI applications must include a %{name}.desktop
> file, and that file must be properly installed with desktop-file-install in the
> %install section.
> OK (Verified on desktop)
> 
> - MUST: Packages must not own files or directories already owned by other
> packages. The rule of thumb here is that the first package to be installed
> should own the files or directories that other packages may rely upon. This
> means, for example, that no package in Fedora should ever share ownership with
> any of the files or directories owned by the filesystem or man package. If you
> feel that you have a good reason to own a file or directory that another package
> owns, then please present that at package review time.
> OK.  I don't know how to check that automatically, but a look using rpmls at the
> binary files looks okay.
> 
> - MUST: At the beginning of %install, each package MUST run rm -rf %{buildroot}
> ([wiki:Self:Packaging/Guidelines#UsingBuildRootOptFlags or $RPM_BUILD_ROOT] ).
> See [wiki:Self:Packaging/Guidelines#PreppingBuildRootForInstall Prepping
> BuildRoot For %install] for details.
> OK
> 
> - MUST: All filenames in rpm packages must be valid UTF-8.
> OK.
> 
> 
> Serious problems:
> * gwhy fails if the .c file isn't in the current directory (home directory if
> invoked from the GUI).

Fixed (change to gwhy.sh, further correction to my patch).

> * In the Zenity patch, use --file-selection not --entry to get the filename.
> That way, people can use a GUI to traverse the directory structure and click on
> the right file.

Changed.

> Strongly recommend fixing:
> * apply "execstack -c" to ELF files in /usr/bin, as noted above. (But only if
> they're ELF, don't do that to bytecode).  That will enable the exec-stack
> protection, there's no reason it should be disabled.

Fixed, see above.

> * In the description, change "Furthermore, in theory," to just "Furthermore". 
> To a lot of people, "in theory" means "not really". Since they've demonstrated
> the truth of the claim for 2 rather different languages, I think they've proved
> that claim.

Changed.

> * By default gwhy gives a HUGE list of potential provers, even when they aren't
> installed.  That's a big pain - you want beginning users to have a reasonable
> view when they start!! In the long term, I think upstream should modify gwhy so
> that at start-up it detects which provers exist, and only shows the ones that
> are installed.  For the short term, can you modify the defaults so that by
> default, if the user hasn't made any selections, only Zenon, Ergo, and CVC3 are
> shown?

Changed, patch to config.ml.

> Other suggestions:
> * Simplify this comment:
>  # Native ocaml builds do not seem to work on ppc64 (not the first
>  # package for which this has been true)
>  to something shorter like this:
>  # Native ocaml builds don't work on ppc64 (many packages have this problem)

Changed.

> * I think you should modify the %files list to use wildcards and %exclude,
> instead of (for example) listing every file in /usr/bin.  It would simplify the
> %files list greatly.  It would also make updates much easier; if a future
> version of the package installs some new files (e.g., in /usr/bin), the spec
> file would be more likely to "just work" if it used wildcards.  E.G., I suggest
> something like this:
> %files
> %{_bindir}/*
> %exclude %{_bindir}/gwhy*
> ...
>  You must _not_ say "%{bindir}/" (that tries to grab /usr/bin itself), but
> %{bindir}/* is fine... and in this case, I think it's preferable.
> 

Fixed.

Also, re:

Most of the SHOULDs don't apply, but I think this one does:
- SHOULD: Usually, subpackages other than devel should require the base package
using a fully versioned dependency.

The subpackages aren't fully versioned.  Is there a reason for that?

Fixed this too.

Let me know what you think (and if you think any more changes would be good).

Comment 13 David A. Wheeler 2008-08-03 02:18:12 UTC
Excellent!

I checked and confirmed that you've fixed the blocker (not including the license file).  rpmlint is now 100% silent (which is good; that means the buffer overflow protection, etc., will now work properly).

I started up the graphical "gwhy" and confirmed that (1) you can now navigate the filesystem using the GUI, and that (2) you can work with files not in the current directory.  Looks good.  I did a try with binary_search.c, and confirmed that it now works with Zenon (which already has a Fedora package).  Zenon doesn't do a _great_ job, but it does prove some verification conditions.  Reducing the number of default columns is a big help; new users will be overwhelmed enough.

I think it's ready for release. Congrats!

APPROVED.

Comment 14 Alan Dunn 2008-08-03 14:58:36 UTC
New Package CVS Request
=======================
Package Name: why
Short Description: Why software verification platform
Owners: amdunn
Branches: F-8 F-9
Cvsextras Commits: yes

Comment 15 Kevin Fenzi 2008-08-04 18:32:17 UTC
cvs done.

Comment 16 Fedora Update System 2008-08-05 21:23:33 UTC
why-2.14-2.fc8.1 has been submitted as an update for Fedora 8

Comment 17 Fedora Update System 2008-08-07 23:56:50 UTC
why-2.14-2.fc8.1 has been pushed to the Fedora 8 stable repository.  If problems still persist, please make note of it in this bug report.


Note You need to log in before you can comment on or make changes to this bug.