[Bug 456398] Review Request: why - Why software verification platform
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=456398 Kevin Fenzi changed: What|Removed |Added Status|NEW |CLOSED Resolution||RAWHIDE -- 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. ___ Fedora-package-review mailing list Fedora-package-review@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=456398 --- Comment #17 from Fedora Update System <[EMAIL PROTECTED]> 2008-08-07 19:56:50 EDT --- 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. -- 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. ___ Fedora-package-review mailing list Fedora-package-review@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=456398 --- Comment #16 from Fedora Update System <[EMAIL PROTECTED]> 2008-08-05 17:23:33 EDT --- why-2.14-2.fc8.1 has been submitted as an update for Fedora 8 -- 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. ___ Fedora-package-review mailing list Fedora-package-review@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=456398 Kevin Fenzi <[EMAIL PROTECTED]> changed: What|Removed |Added CC||[EMAIL PROTECTED] --- Comment #15 from Kevin Fenzi <[EMAIL PROTECTED]> 2008-08-04 14:32:17 EDT --- cvs done. -- 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. ___ Fedora-package-review mailing list Fedora-package-review@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=456398 --- Comment #14 from Alan Dunn <[EMAIL PROTECTED]> 2008-08-03 10:58:36 EDT --- New Package CVS Request === Package Name: why Short Description: Why software verification platform Owners: amdunn Branches: F-8 F-9 Cvsextras Commits: yes -- 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. ___ Fedora-package-review mailing list Fedora-package-review@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
Please do not reply directly to this email. All additional comments should be made in the comments box of this bug. https://bugzilla.redhat.com/show_bug.cgi?id=456398 --- Comment #13 from David A. Wheeler <[EMAIL PROTECTED]> 2008-08-02 22:18:12 EDT --- 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. -- 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. ___ Fedora-package-review mailing list Fedora-package-review@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-08-01 23:24 EST ---
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 a
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-30 23:30 EST --- 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? -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 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
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-30 18:05 EST --- 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. -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-30 14:24 EST ---
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)/
> * 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.
--
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@redhat.com
http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-25 18:19 EST --- (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. -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-25 18:13 EST --- (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. -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-24 17:18 EST --- > * 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? -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-24 16:11 EST --- (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 o
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-23 16:19 EST --- 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. -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] 2008-07-23 14:36 EST --- 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. -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
[Bug 456398] Review Request: why - Why software verification platform
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 [EMAIL PROTECTED] changed: What|Removed |Added AssignedTo|[EMAIL PROTECTED]|[EMAIL PROTECTED] --- Additional Comments From [EMAIL PROTECTED] 2008-07-23 11:54 EST --- Excellent!!! I've wanted this in Fedora for a while, I'll gladly pick up the review. -- 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@redhat.com http://www.redhat.com/mailman/listinfo/fedora-package-review
