Date: Sun, 8 Jun 2014 10:48:10 +0000 (UTC) From: John Marino <marino@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r357001 - head/math/why3-gpl Message-ID: <201406081048.s58AmAMd098318@svn.freebsd.org>
next in thread | raw e-mail | index | archive | help
Author: marino Date: Sun Jun 8 10:48:10 2014 New Revision: 357001 URL: http://svnweb.freebsd.org/changeset/ports/357001 QAT: https://qat.redports.org/buildarchive/r357001/ Log: math/why3-gpl: Increase distinction between this and math/wny3 The why3 project is worried that users will be confused between this package and a "vanilla" why3, which was simultaneously added with this one. They prefer that this port be completely renamed. While I ponder that, I can at least improve the situation by fixing the descriptions to lessen the chance of confusion between the ports. Modified: head/math/why3-gpl/Makefile head/math/why3-gpl/pkg-descr Modified: head/math/why3-gpl/Makefile ============================================================================== --- head/math/why3-gpl/Makefile Sun Jun 8 10:19:25 2014 (r357000) +++ head/math/why3-gpl/Makefile Sun Jun 8 10:48:10 2014 (r357001) @@ -10,7 +10,7 @@ PKGNAMESUFFIX= -gpl DISTNAME= ${PORTNAME}${PKGNAMESUFFIX}-${PORTVERSION}-src MAINTAINER= marino@FreeBSD.org -COMMENT= Deductive program verification platform with SPARK support +COMMENT= Component of SPARK 2014 LICENSE= LGPL21 GPLv3 LICENSE_COMB= multi Modified: head/math/why3-gpl/pkg-descr ============================================================================== --- head/math/why3-gpl/pkg-descr Sun Jun 8 10:19:25 2014 (r357000) +++ head/math/why3-gpl/pkg-descr Sun Jun 8 10:48:10 2014 (r357001) @@ -1,24 +1,5 @@ -Why3 is a platform for deductive program verification. It provides a rich -language for specification and programming, called WhyML, and relies on -external theorem provers, both automated and interactive, to discharge -verification conditions. Why3 comes with a standard library of logical -theories (integer and real arithmetic, Boolean operations, sets and maps, -etc.) and basic programming data structures (arrays, queues, hash tables, -etc.). A user can write WhyML programs directly and get correct-by- -construction OCaml programs through an automated extraction mechanism. -WhyML is also used as an intermediate language for the verification of C, -Java, or Ada programs. - -Why3 is a complete reimplementation of the former Why platform. Among the -new features are: numerous extensions to the input language, a new -architecture for calling external provers, and a well-designed API, -allowing to use Why3 as a software library. An important emphasis is put -on modularity and genericity, giving the end user a possibility to easily -reuse Why3 formalizations or to add support for a new external prover if -wanted. - -This GPL version version of Why3 has been released by Adacore with an -additional binary for SPARK 2014 support and some patches which have not -yet been pushed upstream. +This is a component of SPARK 2014. Those looking for the deductive +program verification platform known as why3 should refer to math/why3 +instead. WWW: https://forge.open-do.org/projects/spark2014
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201406081048.s58AmAMd098318>