Bug 487094 - Review Request: stp - Constraint solver/decision procedure
Summary: Review Request: stp - Constraint solver/decision procedure
Keywords:
Status: CLOSED NEXTRELEASE
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Marcela Mašláňová
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2009-02-24 05:28 UTC by David A. Wheeler
Modified: 2009-03-09 22:59 UTC (History)
2 users (show)

Fixed In Version: 0.1-4.fc10
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2009-03-09 22:59:21 UTC
Type: ---
Embargoed:
mmaslano: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description David A. Wheeler 2009-02-24 05:28:51 UTC
Spec URL: http://www.dwheeler.com/stp.spec
SRPM URL: http://www.dwheeler.com/stp-0.1-1.fc10.src.rpm
Description: 
STP (Simple Theorem Prover) is
a constraint solver (also referred to as a decision procedure
or automated prover) aimed at solving constraints generated by program
analysis tools, theorem provers, automated bug finders, intelligent
fuzzers and model checkers. STP has been used in many research projects
at Stanford, Berkeley, MIT, CMU and other universities, as well as
companies and government agencies.

The input to STP are formulas over the theory of bit-vectors and arrays
(This theory captures most expressions from languages like C/C++/Java
and Verilog), and the output of STP is a single bit of information that
indicates whether the formula is satisfiable or not. If the input is
satisfiable, then it also generates a variable assignment to satisfy
the input formula.

Additional information can be found at:
 http://people.csail.mit.edu/vganesh/STP_files/stp.html


Koji builds okay: http://koji.fedoraproject.org/koji/taskinfo?taskID=1151367
  0 free  0 open  5 done  0 failed

rpmlint is happy too.

Comment 1 Marcela Mašláňová 2009-02-26 11:28:49 UTC
OK Rpmlint must be run on every package.
OK The package must be named according to the Package Naming Guidelines .
OK The spec file name must match the base package %{name}.
OK The package must meet the Packaging Guidelines.
OK The package must be licensed with a Fedora approved license.
OK The License field in the package spec file must match the actual license.
OK If (and only if) the source package includes the text of the license(s) in its own file.
OK The spec file must be written in American English.
OK The spec file for the package MUST be legible.
OK The sources used to build the package must match the upstream source.
OK The package MUST successfully compile.
OK Correct BuildRequires.
OK Proper use of %find_lang macro. Using %{_datadir}/locale/* is strictly forbidden.
OK Shared library files (not just symlinks) must call ldconfig in %post and %postun.
OK Relocatable package must state this fact in the request for review.
OK A package must own all directories that it creates.
OK A package must not contain any duplicate files in the %files listing.
OK Permissions on files must be set properly.
OK Each package must have a %clean section, which contains rm -rf %{buildroot} (or $RPM_BUILD_ROOT).
OK Each package must consistently use macros.
OK The package must contain code, or permissable content.
OK Large documentation files must go in a -doc subpackage.
OK If a package includes something as %doc, it must not affect the runtime of the application.
OK Header files must be in a -devel package.
OK Static libraries must be in a -static package.
OK Packages containing pkgconfig(.pc) files must 'Requires: pkgconfig'.
OK Library files with a suffix (e.g. libfoo.so.1.1) and files that end in .so (without suffix) must go in -devel.
OK In the vast majority of cases, devel packages must require the base package.
OK Packages must NOT contain any .la libtool archives.
OK Packages containing GUI applications must include a %{name}.desktop file.
OK At the beginning of %install, each package MUST run rm -rf %{buildroot} (or $RPM_BUILD_ROOT).

Usually are all packages and subpackages on the top of spec and check part is placed before %files. This is little confusing. 
It's better to use macro for release version 0.1-11-18-2008 for future updates.
Also you don't have to create doc for devel package, it the base package includes them and it's required by devel package.

Comment 2 David A. Wheeler 2009-03-03 14:35:18 UTC
Okay, posted updated .spec/SRPM.  Moved stuff around, used a macro (using %global not %define as suggested by some draft guidance), and removed the dup document file.

Hope it's all okay now.  I did scratch koji builds for both dist-f10 and dist-f11, and it works for both versions on all architectures:
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=1216922
  0 free  0 open  5 done  0 failed
Task info: http://koji.fedoraproject.org/koji/taskinfo?taskID=1216974
  0 free  0 open  5 done  0 failed

rpmlint is clean for the .spec file, SRPM, and a binary RPM (stp-0.1-2.fc11.i586.rpm).

Here are the new versions:
http://www.dwheeler.com/stp.spec
http://www.dwheeler.com/stp-0.1-2.fc10.src.rpm

Comment 3 Marcela Mašláňová 2009-03-03 15:04:31 UTC
ACCEPTED

Comment 4 David A. Wheeler 2009-03-04 03:53:50 UTC
New Package CVS Request
=======================
Package Name: stp
Short Description: Constraint solver/decision procedure
Owners: dwheeler amdunn
Branches: F-10
InitialCC:

Comment 5 Kevin Fenzi 2009-03-05 20:13:04 UTC
cvs done.

Comment 6 Fedora Update System 2009-03-06 06:41:39 UTC
stp-0.1-4.fc10 has been submitted as an update for Fedora 10.
http://admin.fedoraproject.org/updates/stp-0.1-4.fc10

Comment 7 Fedora Update System 2009-03-09 22:59:16 UTC
stp-0.1-4.fc10 has been pushed to the Fedora 10 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.