Please do not reply directly to this email. All additional comments should be made in the comments box of this bug report. Summary: Review Request: why - Why software verification platform https://bugzilla.redhat.com/show_bug.cgi?id=456398 ------- Additional Comments From dwheeler@xxxxxxxxxxxx 2008-07-30 23:26 EST ------- 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. -- Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email ------- You are receiving this mail because: ------- You are on the CC list for the bug, or are watching someone who is. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review