cpet/freebsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

math/why3-gpl: Increase distinction between this and math/wny3

Browse Source 
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.
This commit is contained in:
John Marino 2014-06-08 10:48:10 +00:00
parent cd03765d17
commit 03ec223fd7
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=357001
2 changed files with 4 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
math/why3-gpl/Makefile
View File

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

25
math/why3-gpl/pkg-descr
View File

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