svn commit: r357001 - head/math/why3-gpl

[John Marino]

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 at 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