Bug 768538

Summary: Review Request: why3 - Software verification platform
Product: [Fedora] Fedora Reporter: Jerry James <loganjerry>
Component: Package ReviewAssignee: Gwyn Ciesla <gwync>
Status: CLOSED ERRATA QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: medium Docs Contact:
Priority: medium    
Version: rawhideCC: gwync, notting, package-review
Target Milestone: ---Flags: gwync: fedora-review+
gwync: fedora-cvs+
Target Release: ---   
Hardware: All   
OS: Linux   
Whiteboard:
Fixed In Version: why3-0.71-2.fc16 Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2012-04-29 01:02:31 UTC Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:
Bug Depends On: 754245    
Bug Blocks:    

Description Jerry James 2011-12-16 22:46:39 UTC
Spec URL: http://jjames.fedorapeople.org/why3/why3.spec
SRPM URL: http://jjames.fedorapeople.org/why3/why3-0.71-1.fc16.src.rpm
Description: Why3 is the next generation of the Why software verification platform.  Why3 clearly separates the purely logical specification part from generation of verification conditions for programs.  It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Fedora note: while why3 is the eventual successor to the existing why package, right now both are needed.  The current version of why can be used by itself, but if why3 is also installed, some of its more powerful reasoning features can be used.  On the flip side, why3 isn't yet complete.  Upstream recommends that the two versions be used side by side for now.

Comment 1 Gwyn Ciesla 2012-04-09 20:18:17 UTC
Good:

- rpmlint checks return: 

why3.src: W: spelling-error %description -l en_US provers -> proves, rovers, proverbs
The value of this tag appears to be misspelled. Please double-check.

Ignore.

why3-emacs.noarch: W: no-documentation
The package contains no documentation (README, doc, etc). You have to include
documentation files.

why3-emacs-el.noarch: W: no-documentation
The package contains no documentation (README, doc, etc). You have to include
documentation files.

why3-xemacs.noarch: W: no-documentation
The package contains no documentation (README, doc, etc). You have to include
documentation files.

why3-xemacs-el.noarch: W: no-documentation
The package contains no documentation (README, doc, etc). You have to include
documentation files.

why3.x86_64: W: no-manual-page-for-binary why3-cpulimit
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3ml
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3config
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3bench
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3realize
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3replayer
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3doc
Each executable in standard binary directories should have a man page.

why3.x86_64: W: no-manual-page-for-binary why3ide
Each executable in standard binary directories should have a man page.

why3-all.x86_64: W: no-documentation
The package contains no documentation (README, doc, etc). You have to include
documentation files.

why3-coq.x86_64: W: no-documentation
The package contains no documentation (README, doc, etc). You have to include
documentation files.

Fix if possbile, examine at least.

- package meets naming guidelines
- package meets packaging guidelines
- license ( LGPLv2 with exceptions ) OK, text in %doc, matches source
- spec file legible, in am. english
- source matches upstream
- package compiles on devel (x86_64)
- no missing BR

Mock rawhide build fails, missing BuildRequires on sqlite-devel.  After that it's fine.

- no unnecessary BR
- no locales
- not relocatable
- owns all directories that it creates
- no duplicate files
- permissions ok
- %clean ok
- macro use consistent
- code, not content
- no need for -docs
- nothing in %doc affects runtime
- no need for .desktop file

Comment on why debuginfo is disabled, or enable it.

Comment 2 Gwyn Ciesla 2012-04-18 13:19:17 UTC
Ping?

Comment 3 Jerry James 2012-04-19 16:35:12 UTC
Sorry, I was out of town for a little over a week.  I thought I'd do some package work in the evenings, but kept getting back to my room quite late and very tired.  Here's a new build that I believe fixes all of the issues noted above, including the addition of some man pages.

Spec URL: http://jjames.fedorapeople.org/why3/why3.spec
SRPM URL: http://jjames.fedorapeople.org/why3/why3-0.71-2.fc16.src.rpm

Comment 4 Gwyn Ciesla 2012-04-19 17:34:11 UTC
No worries, been there. :)

Looks great now, APPROVED.  Thanks!

Comment 5 Jerry James 2012-04-19 18:40:51 UTC
Thanks for the review, Jon.

New Package SCM Request
=======================
Package Name: why3
Short Description: Software verification platform
Owners: jjames
Branches: f16 f17
InitialCC:

Comment 6 Gwyn Ciesla 2012-04-19 18:50:33 UTC
Git done (by process-git-requests).

Comment 7 Fedora Update System 2012-04-19 20:06:04 UTC
why3-0.71-2.fc17 has been submitted as an update for Fedora 17.
https://admin.fedoraproject.org/updates/why3-0.71-2.fc17

Comment 8 Fedora Update System 2012-04-19 20:06:33 UTC
why3-0.71-2.fc16 has been submitted as an update for Fedora 16.
https://admin.fedoraproject.org/updates/why3-0.71-2.fc16

Comment 9 Fedora Update System 2012-04-20 06:03:29 UTC
why3-0.71-2.fc17 has been pushed to the Fedora 17 testing repository.

Comment 10 Fedora Update System 2012-04-29 01:02:31 UTC
why3-0.71-2.fc17 has been pushed to the Fedora 17 stable repository.

Comment 11 Fedora Update System 2012-05-01 00:48:24 UTC
why3-0.71-2.fc16 has been pushed to the Fedora 16 stable repository.