From owner-svn-ports-all@FreeBSD.ORG Sun Jun 8 10:48:11 2014 Return-Path: Delivered-To: svn-ports-all@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [8.8.178.115]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by hub.freebsd.org (Postfix) with ESMTPS id E55A7FD2; Sun, 8 Jun 2014 10:48:10 +0000 (UTC) Received: from svn.freebsd.org (svn.freebsd.org [IPv6:2001:1900:2254:2068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id C620928C9; Sun, 8 Jun 2014 10:48:10 +0000 (UTC) Received: from svn.freebsd.org ([127.0.1.70]) by svn.freebsd.org (8.14.8/8.14.8) with ESMTP id s58AmAXY098320; Sun, 8 Jun 2014 10:48:10 GMT (envelope-from marino@svn.freebsd.org) Received: (from marino@localhost) by svn.freebsd.org (8.14.8/8.14.8/Submit) id s58AmAMd098318; Sun, 8 Jun 2014 10:48:10 GMT (envelope-from marino@svn.freebsd.org) Message-Id: <201406081048.s58AmAMd098318@svn.freebsd.org> From: John Marino Date: Sun, 8 Jun 2014 10:48:10 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r357001 - head/math/why3-gpl X-SVN-Group: ports-head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-all@freebsd.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: SVN commit messages for the ports tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 08 Jun 2014 10:48:11 -0000 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