kpriv/pkgsrc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
pkgsrc/devel/spin/Makefile

25 lines
621 B
Makefile
Raw Normal View History

Drop superfluous PKG_DESTDIR_SUPPORT, "user-destdir" is default these days.
2012-10-31 12:16:30 +01:00
# $NetBSD: Makefile,v 1.3 2012/10/31 11:19:47 asau Exp $
Initial import of spin version 5.2.5 into the Packages Collection. To verify a design, a formal model is built using PROMELA, Spin's input language. PROMELA is a non-deterministic language, loosely based on Dijkstra's guarded command language notation and borrowing the notation for I/O operations from Hoare's CSP language. Spin can be used in four main modes: 1. as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations 2. as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search) 3. as proof approximation system that can validate even very large system models with maximal coverage of the state space. 4. as a driver for swarm verification (a new form of swarm computing), which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models. With thanks to the plan9 guys for the nudge
2010-10-24 20:54:12 +02:00
DISTNAME= spin525
PKGNAME= spin-5.2.5
CATEGORIES= devel
MASTER_SITES= http://spinroot.com/spin/Src/
MAINTAINER= agc@NetBSD.org
HOMEPAGE= http://spinroot.com/spin/whatispin.html
COMMENT= Formal correctness prover
LICENSE= spin-license
INSTALLATION_DIRS= bin ${PKGMANDIR}/man1
WRKSRC= ${WRKDIR}/Spin/Src5.2.5
Needs yacc; seen in the Linux build report.
2012-06-18 05:42:25 +02:00
USE_TOOLS+= yacc
Initial import of spin version 5.2.5 into the Packages Collection. To verify a design, a formal model is built using PROMELA, Spin's input language. PROMELA is a non-deterministic language, loosely based on Dijkstra's guarded command language notation and borrowing the notation for I/O operations from Hoare's CSP language. Spin can be used in four main modes: 1. as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations 2. as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search) 3. as proof approximation system that can validate even very large system models with maximal coverage of the state space. 4. as a driver for swarm verification (a new form of swarm computing), which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models. With thanks to the plan9 guys for the nudge
2010-10-24 20:54:12 +02:00
MAKE_FILE= makefile
BUILD_TARGET= spin
do-install:
${INSTALL_PROGRAM} ${WRKSRC}/spin ${DESTDIR}${PREFIX}/bin/spin
${INSTALL_MAN} ${WRKDIR}/Spin/Man/spin.1 ${DESTDIR}${PREFIX}/${PKGMANDIR}/man1/spin.1
.include "../../mk/bsd.pkg.mk"
Reference in a new issue Copy permalink