Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 111542 - New package: spin (formal software systems verification tool)
Summary: New package: spin (formal software systems verification tool)
Status: CONFIRMED
Alias: None
Product: Gentoo Linux
Classification: Unclassified
Component: New packages (show other bugs)
Hardware: All Linux
: Normal normal (vote)
Assignee: Default Assignee for New Packages
URL: http://spinroot.com/
Whiteboard: sunrise suggested
Keywords: EBUILD
Depends on:
Blocks:
 
Reported: 2005-11-05 04:52 UTC by Christian Schlotter
Modified: 2018-06-07 18:25 UTC (History)
1 user (show)

See Also:
Package list:
Runtime testing required: ---


Attachments
spin-4.2.6.ebuild (spin-4.2.6.ebuild,1.66 KB, text/plain)
2005-11-05 04:53 UTC, Christian Schlotter
Details
spin-4.2.6-xspin_wish_path.patch (spin-4.2.6-xspin_wish_path.patch,316 bytes, patch)
2005-11-05 04:53 UTC, Christian Schlotter
Details | Diff
SPIN public license (spin,18.81 KB, text/plain)
2005-11-05 04:56 UTC, Christian Schlotter
Details
spin-4.2.6.ebuild (spin-4.2.6.ebuild,1.66 KB, text/plain)
2005-11-05 05:00 UTC, Christian Schlotter
Details
spin-4.2.6.ebuild (spin-4.2.6.ebuild,1.68 KB, text/plain)
2005-11-05 16:26 UTC, Christian Schlotter
Details
spin-4.2.6.ebuild (spin-4.2.6.ebuild,1.74 KB, text/plain)
2005-11-06 05:45 UTC, Christian Schlotter
Details
spin-4.2.6-xspin_time_not_found.patch (spin-4.2.6-xspin_time_not_found.patch,291 bytes, patch)
2005-11-06 05:47 UTC, Christian Schlotter
Details | Diff
spin-4.2.6.ebuild (spin-4.2.6.ebuild,1.81 KB, text/plain)
2005-11-08 13:11 UTC, Christian Schlotter
Details
spin-4.2.7 Package (contains portage tree directory) (spin.tar.gz,8.87 KB, application/x-gzip)
2006-10-16 13:10 UTC, joes5532
Details
SPIN-Commercial (needs to go in /usr/portage/licenses) (SPIN-Commercial,18.87 KB, text/plain)
2006-10-17 13:10 UTC, joes5532
Details
spin-5.2.2 ebuild with hierarchy (spin.tar.gz,8.79 KB, application/octet-stream)
2009-09-23 14:25 UTC, Felix Wieczorek
Details
spin 5.2.2 ebuild with patch for time (spin-5.2.2-r1.ebuild,1.34 KB, text/plain)
2009-11-11 14:12 UTC, Felix Wieczorek
Details
in xspin there is an error, because of the syntax in the time statement, just deactivated it (spin-5.2.2-xspin_time.patch,728 bytes, patch)
2009-11-11 14:14 UTC, Felix Wieczorek
Details | Diff

Note You need to log in before you can comment on or make changes to this bug.
Description Christian Schlotter 2005-11-05 04:52:18 UTC
Hello!

Please find attached the ebuild plus needed files for a new package: spin.  I
also attached the commercial license which should be put into
/usr/portage/licenses.  For genereal use of spin, no license is required.

About spin (from the homepage):
Spin is a popular open-source software tool, used by thousands of people
worldwide, that can be used for the formal verification of distributed software
systems. The tool was developed at Bell Labs in the original Unix group of the
Computing Sciences Research Center, starting in 1980. The software has been
available freely since 1991, and continues to evolve to keep pace with new
developments in the field. In April 2002 the tool was awarded the prestigious
System Software Award for 2001 by the ACM.

I suggest sci-misc/spin.

Best regards
Christian
Comment 1 Christian Schlotter 2005-11-05 04:53:12 UTC
Created attachment 72164 [details]
spin-4.2.6.ebuild
Comment 2 Christian Schlotter 2005-11-05 04:53:51 UTC
Created attachment 72165 [details, diff]
spin-4.2.6-xspin_wish_path.patch
Comment 3 Christian Schlotter 2005-11-05 04:56:37 UTC
Created attachment 72166 [details]
SPIN public license

http://cm.bell-labs.com/cm/cs/what/spin/SPIN_public_license.txt

From README.html:
"Spin is distributed in source form to encourage research in formal
verification, and to help a support friendly and open exchange of algorithms,
ideas, and tools. The software itself has a copyright from Lucent Technologies
and Bell Laboratories, and is distributed for research and educational purposes
only (i.e., no guarantee of any kind is implied by the distribution of the
code, and all rights are reserved by the copyright holder). For this general
use of Spin, no license is required.

Commercial application of the Spin software is also allowed, but requires the
acceptance of a basic license. Refer to the Spin Public license for details."
Comment 4 Christian Schlotter 2005-11-05 05:00:30 UTC
Created attachment 72168 [details]
spin-4.2.6.ebuild

cleanup
Comment 5 Christian Schlotter 2005-11-05 16:26:11 UTC
Created attachment 72251 [details]
spin-4.2.6.ebuild

RDEPEND update
Comment 6 Christian Schlotter 2005-11-06 05:45:58 UTC
Created attachment 72282 [details]
spin-4.2.6.ebuild
Comment 7 Christian Schlotter 2005-11-06 05:47:46 UTC
Created attachment 72283 [details, diff]
spin-4.2.6-xspin_time_not_found.patch

This was needed because on my system "time" is not an executable, but a
reserved word in bash.
Comment 8 Christian Schlotter 2005-11-08 13:11:20 UTC
Created attachment 72467 [details]
spin-4.2.6.ebuild

Change:
xspin has the optional runtime dependency graphviz.  It detects automatically
if dot (provided by graphviz) is present.
Comment 9 Ceesjan Luiten 2006-10-10 06:54:47 UTC
Thank you for your ebuild Christian Schlotter :)

Spin 4.2.7 has been released, Schlotters ebuild can be used by :

1) Renaming spin-4.2.6 to spin-4.2.7.ebuild
2) Within the ebuild, line 7, replacing MY_PV="426" with MY_PV="427"
3) Within the patches, renaming xspin426.tcl to xspin427.tcl (twice for each patch)

Then it installs and seems to be working OK.
Comment 10 joes5532 2006-10-16 13:10:48 UTC
Created attachment 99827 [details]
spin-4.2.7 Package (contains portage tree directory)

I had noticed that there was no ebuild for Spin in the tree, so I just spent an hour making one for version 4.2.7.  Then when I was going to post it, I did a search and saw all the wonderful work you guys have already done :)  Nonetheless, here is my contribution.  I haven't made any attempts to sync it up with your existing 4.2.6 ebuild, but it takes care of all the features, including Xspin, dot, and it even presents the user with the license, which they must accept before continuing!

To use this package, untar it into your /usr/local/portage directory.  Make sure you have set PORTDIR_OVERLAY="/usr/local/portage" in /etc/make.conf too.  There are two USE flags, 'xspin' and 'dot', which will install Xspin and Graphviz for dot, respectively.  To set the flags just for this package, add a line in /etc/portage/package.use that says 'sci-mathematics/spin xspin dot'.  That's it!

Cheers,
Jeff
Comment 11 Christian Schlotter 2006-10-17 04:38:10 UTC
(In reply to comment #9)
> 2) Within the ebuild, line 7, replacing MY_PV="426" with MY_PV="427"

An improvement would be to replace line 7 with
MY_PV=${PV//.}

(In reply to comment #10)

Thanks for your contribution, Jeff!
Comment 12 joes5532 2006-10-17 13:09:31 UTC
I realize after talking with someone that we're not supposed to include the license like I did.  It should already be a part of /usr/portage/licenses.  So does anyone know how to go about adding a license?  We need to add "SPIN-Commercial" to the licenses.  I've attached the license text file to this bug.

Cheers,
Jeff
Comment 13 joes5532 2006-10-17 13:10:43 UTC
Created attachment 99896 [details]
SPIN-Commercial (needs to go in /usr/portage/licenses)
Comment 14 joes5532 2006-10-18 21:19:58 UTC
You could just use the methods of the versionator eclass to do this as well.  That way you don't need to define MY_PV; you can just work with ${PV} instead.

(In reply to comment #11)
> (In reply to comment #9)
> > 2) Within the ebuild, line 7, replacing MY_PV="426" with MY_PV="427"
> 
> An improvement would be to replace line 7 with
> MY_PV=${PV//.}
> 
> (In reply to comment #10)
> 
> Thanks for your contribution, Jeff!
> 

Comment 15 Jeremy Olexa (darkside) (RETIRED) archtester gentoo-dev Security 2009-02-28 04:19:20 UTC
(this is an automated message based on filtering criteria that matched this bug)
'EBUILD' is in the KEYWORDS which should mean that there is a ebuild attached 
to this bug.
This bug is assigned to maintainer-wanted which means that it is not in the 
main tree.
Heuristics show that no Gentoo developer has commented on your ebuild.

Hello, The Gentoo Team would like to firstly thank you for your ebuild 
submission. We also apologize for not being able to accommodate you in a timely
manner. There are simply too many new packages.

Allow me to use this opportunity to introduce you to Gentoo Sunrise. The 
sunrise overlay[1] is a overlay for Gentoo which we allow trusted users to 
commit to and all users can have ebuilds reviewed by Gentoo devs for entry 
into the overlay. So, the sunrise team is suggesting that you look into this 
and submit your ebuild to the overlay where even *you* can commit to. =)

Because this is a mass message, we are also asking you to be patient with us. 
We anticipate a large number of requests in a short time. 

Thanks,
On behalf of the Gentoo Sunrise Team,
Jeremy.

[1]: http://www.gentoo.org/proj/en/sunrise/
[2]: http://overlays.gentoo.org/proj/sunrise/wiki/SunriseFaq
Comment 16 Felix Wieczorek 2009-09-23 14:25:32 UTC
Created attachment 205022 [details]
spin-5.2.2 ebuild with hierarchy

I today altered the ebuild to the new version (5.2.2). It's my first ebuild, advise and corrections are welcome.
Comment 17 Felix Wieczorek 2009-11-11 14:11:24 UTC
modified the ebuild, got rid of the sed calls in ebuild and adapted the time_patch of Christian Schlotter
Comment 18 Felix Wieczorek 2009-11-11 14:12:34 UTC
Created attachment 209909 [details]
spin 5.2.2 ebuild with patch for time
Comment 19 Felix Wieczorek 2009-11-11 14:14:53 UTC
Created attachment 209910 [details, diff]
in xspin there is an error, because of the syntax in the time statement, just deactivated it