diff options
Diffstat (limited to 'math/why3-gpl')
| -rw-r--r-- | math/why3-gpl/Makefile | 21 | ||||
| -rw-r--r-- | math/why3-gpl/distinfo | 2 | ||||
| -rw-r--r-- | math/why3-gpl/files/patch-Makefile.in | 10 | ||||
| -rw-r--r-- | math/why3-gpl/files/patch-src_tools_cpulimit.c | 10 | ||||
| -rw-r--r-- | math/why3-gpl/pkg-descr | 24 | ||||
| -rw-r--r-- | math/why3-gpl/pkg-plist | 199 |
6 files changed, 266 insertions, 0 deletions
diff --git a/math/why3-gpl/Makefile b/math/why3-gpl/Makefile new file mode 100644 index 000000000000..fed0023d6833 --- /dev/null +++ b/math/why3-gpl/Makefile @@ -0,0 +1,21 @@ +# Created by: John Marino <marino@FreeBSD.org> +# $FreeBSD$ + +PORTNAME= why3 +PORTVERSION= 2014 +CATEGORIES= math +MASTER_SITES= http://downloads.dragonlace.net/src/ \ + LOCAL/marino +PKGNAMESUFFIX= -gpl +DISTNAME= ${PORTNAME}${PKGNAMESUFFIX}-${PORTVERSION}-src + +MAINTAINER= marino@FreeBSD.org +COMMENT= Deductive program verification platform with SPARK support + +LICENSE= LGPL21 GPLv3 +LICENSE_COMB= multi + +ALL_TARGET= all + +.include "${.CURDIR}/../why3/Makefile.common" +.include <bsd.port.mk> diff --git a/math/why3-gpl/distinfo b/math/why3-gpl/distinfo new file mode 100644 index 000000000000..2d7f02295e15 --- /dev/null +++ b/math/why3-gpl/distinfo @@ -0,0 +1,2 @@ +SHA256 (why3-gpl-2014-src.tar.gz) = 0f598327b3c27f98bc7064929d990d422303155d106b1d9eb48246c039415e9e +SIZE (why3-gpl-2014-src.tar.gz) = 4568701 diff --git a/math/why3-gpl/files/patch-Makefile.in b/math/why3-gpl/files/patch-Makefile.in new file mode 100644 index 000000000000..6d87243ab3a5 --- /dev/null +++ b/math/why3-gpl/files/patch-Makefile.in @@ -0,0 +1,10 @@ +--- Makefile.in.orig 2014-04-03 10:14:03.000000000 +0000 ++++ Makefile.in +@@ -46,7 +46,6 @@ OCAMLLIB = @OCAMLLIB@ + OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@ + OCAMLBEST = @OCAMLBEST@ + OCAMLVERSION = @OCAMLVERSION@ +-CC = gcc + COQC = @COQC@ + COQDEP = @COQDEP@ + CAMLP5O = @CAMLP5O@ diff --git a/math/why3-gpl/files/patch-src_tools_cpulimit.c b/math/why3-gpl/files/patch-src_tools_cpulimit.c new file mode 100644 index 000000000000..5c905ece014a --- /dev/null +++ b/math/why3-gpl/files/patch-src_tools_cpulimit.c @@ -0,0 +1,10 @@ +--- src/tools/cpulimit.c.orig 2014-03-14 15:01:03.000000000 +0000 ++++ src/tools/cpulimit.c +@@ -18,6 +18,7 @@ + #include <stdlib.h> + #include <unistd.h> + #include <errno.h> ++#include <signal.h> + #include <string.h> + #include <sys/wait.h> + diff --git a/math/why3-gpl/pkg-descr b/math/why3-gpl/pkg-descr new file mode 100644 index 000000000000..4ab076ae7288 --- /dev/null +++ b/math/why3-gpl/pkg-descr @@ -0,0 +1,24 @@ +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. + +WWW: https://forge.open-do.org/projects/spark2014 diff --git a/math/why3-gpl/pkg-plist b/math/why3-gpl/pkg-plist new file mode 100644 index 000000000000..0a6644c4773b --- /dev/null +++ b/math/why3-gpl/pkg-plist @@ -0,0 +1,199 @@ +bin/gnatwhy3 +bin/why3 +bin/why3-cpulimit +bin/why3bench +bin/why3config +bin/why3doc +bin/why3ide +bin/why3replayer +bin/why3session +%%OCAML_SITELIBDIR%%/why3/META +%%OCAML_SITELIBDIR%%/why3/why3.a +%%OCAML_SITELIBDIR%%/why3/why3.cmi +%%OCAML_SITELIBDIR%%/why3/why3.cmx +%%OCAML_SITELIBDIR%%/why3/why3.cmxa +%%OCAML_SITELIBDIR%%/why3/why3.o +%%OCAML_SITELIBDIR%%/why3/why3extract.a +%%OCAML_SITELIBDIR%%/why3/why3extract.cmi +%%OCAML_SITELIBDIR%%/why3/why3extract.cmx +%%OCAML_SITELIBDIR%%/why3/why3extract.cmxa +%%OCAML_SITELIBDIR%%/why3/why3extract.o +lib/why3/plugins/dimacs.cmxs +lib/why3/plugins/genequlin.cmxs +lib/why3/plugins/hypothesis_selection.cmxs +lib/why3/plugins/tptp.cmxs +lib/why3/why3-call-pvs +%%DATADIR%%/drivers/alt_ergo.drv +%%DATADIR%%/drivers/alt_ergo_0.92.drv +%%DATADIR%%/drivers/alt_ergo_0.93.drv +%%DATADIR%%/drivers/alt_ergo_0.94.drv +%%DATADIR%%/drivers/alt_ergo_bare.drv +%%DATADIR%%/drivers/alt_ergo_model.drv +%%DATADIR%%/drivers/alt_ergo_smt2.drv +%%DATADIR%%/drivers/beagle.drv +%%DATADIR%%/drivers/coq-common.gen +%%DATADIR%%/drivers/coq-realizations.aux +%%DATADIR%%/drivers/coq-realize.drv +%%DATADIR%%/drivers/coq.drv +%%DATADIR%%/drivers/coq_8_4.drv +%%DATADIR%%/drivers/cvc3.drv +%%DATADIR%%/drivers/cvc3_bare.drv +%%DATADIR%%/drivers/cvc4.drv +%%DATADIR%%/drivers/cvc4_bare.drv +%%DATADIR%%/drivers/cvc4_gnatprove.drv +%%DATADIR%%/drivers/discrimination.gen +%%DATADIR%%/drivers/eprover.drv +%%DATADIR%%/drivers/gappa.drv +%%DATADIR%%/drivers/iprover.drv +%%DATADIR%%/drivers/isabelle-common.gen +%%DATADIR%%/drivers/isabelle-realizations.aux +%%DATADIR%%/drivers/isabelle-realize.drv +%%DATADIR%%/drivers/isabelle.drv +%%DATADIR%%/drivers/mathematica.drv +%%DATADIR%%/drivers/mathsat.drv +%%DATADIR%%/drivers/metis.drv +%%DATADIR%%/drivers/metitarski.drv +%%DATADIR%%/drivers/ocaml-gen.drv +%%DATADIR%%/drivers/ocaml32.drv +%%DATADIR%%/drivers/ocaml64.drv +%%DATADIR%%/drivers/princess.drv +%%DATADIR%%/drivers/pvs-common.gen +%%DATADIR%%/drivers/pvs-realizations.aux +%%DATADIR%%/drivers/pvs-realize.drv +%%DATADIR%%/drivers/pvs.drv +%%DATADIR%%/drivers/simplify.drv +%%DATADIR%%/drivers/spass.drv +%%DATADIR%%/drivers/spass_types.drv +%%DATADIR%%/drivers/tptp-tff0.drv +%%DATADIR%%/drivers/tptp-tff1.drv +%%DATADIR%%/drivers/tptp.gen +%%DATADIR%%/drivers/vampire.drv +%%DATADIR%%/drivers/verit.drv +%%DATADIR%%/drivers/why3.drv +%%DATADIR%%/drivers/why3_smt.drv +%%DATADIR%%/drivers/why3_tptp.drv +%%DATADIR%%/drivers/yices.drv +%%DATADIR%%/drivers/yices_bare.drv +%%DATADIR%%/drivers/z3.drv +%%DATADIR%%/drivers/z3_bare.drv +%%DATADIR%%/drivers/z3_smtv1.drv +%%DATADIR%%/drivers/zenon.drv +%%DATADIR%%/emacs/why3-mode.el +%%DATADIR%%/images/boomy/accept32.png +%%DATADIR%%/images/boomy/bug32.png +%%DATADIR%%/images/boomy/clock32.png +%%DATADIR%%/images/boomy/configure16.png +%%DATADIR%%/images/boomy/configure32.png +%%DATADIR%%/images/boomy/cut32.png +%%DATADIR%%/images/boomy/cutb32.png +%%DATADIR%%/images/boomy/delete32.png +%%DATADIR%%/images/boomy/deletefile32.png +%%DATADIR%%/images/boomy/edit32.png +%%DATADIR%%/images/boomy/file16.png +%%DATADIR%%/images/boomy/file32.png +%%DATADIR%%/images/boomy/folder16.png +%%DATADIR%%/images/boomy/folder32.png +%%DATADIR%%/images/boomy/help32.png +%%DATADIR%%/images/boomy/movefile32.png +%%DATADIR%%/images/boomy/obsaccept32.png +%%DATADIR%%/images/boomy/obsbug32.png +%%DATADIR%%/images/boomy/obsclock32.png +%%DATADIR%%/images/boomy/obsdelete32.png +%%DATADIR%%/images/boomy/obsdeletefile32.png +%%DATADIR%%/images/boomy/obshelp32.png +%%DATADIR%%/images/boomy/pause32.png +%%DATADIR%%/images/boomy/pausehalf32.png +%%DATADIR%%/images/boomy/play32.png +%%DATADIR%%/images/boomy/refresh32.png +%%DATADIR%%/images/boomy/stop32.png +%%DATADIR%%/images/boomy/transformation32.png +%%DATADIR%%/images/boomy/trashb32.png +%%DATADIR%%/images/boomy/undone32.png +%%DATADIR%%/images/boomy/wizard16.png +%%DATADIR%%/images/boomy/wizard32.png +%%DATADIR%%/images/fatcow/accept.png +%%DATADIR%%/images/fatcow/bin.png +%%DATADIR%%/images/fatcow/bomb.png +%%DATADIR%%/images/fatcow/bullet_black.png +%%DATADIR%%/images/fatcow/bullet_blue.png +%%DATADIR%%/images/fatcow/bullet_green.png +%%DATADIR%%/images/fatcow/bullet_red.png +%%DATADIR%%/images/fatcow/bullet_white.png +%%DATADIR%%/images/fatcow/cancel.png +%%DATADIR%%/images/fatcow/control_pause_blue.png +%%DATADIR%%/images/fatcow/control_play_blue.png +%%DATADIR%%/images/fatcow/ddr_memory.png +%%DATADIR%%/images/fatcow/delete.png +%%DATADIR%%/images/fatcow/exclamation.png +%%DATADIR%%/images/fatcow/folder.png +%%DATADIR%%/images/fatcow/help.png +%%DATADIR%%/images/fatcow/magic_wand_2.png +%%DATADIR%%/images/fatcow/multitool.png +%%DATADIR%%/images/fatcow/package.png +%%DATADIR%%/images/fatcow/pencil.png +%%DATADIR%%/images/fatcow/script.png +%%DATADIR%%/images/fatcow/timeline.png +%%DATADIR%%/images/fatcow/update.png +%%DATADIR%%/images/icons.rc +%%DATADIR%%/images/logo-why.png +%%DATADIR%%/javascript/jquery.js +%%DATADIR%%/javascript/jquery.jstree.js +%%DATADIR%%/javascript/session.css +%%DATADIR%%/javascript/session.js +%%DATADIR%%/javascript/themes/default/d.gif +%%DATADIR%%/javascript/themes/default/d.png +%%DATADIR%%/javascript/themes/default/style.css +%%DATADIR%%/javascript/themes/default/throbber.gif +%%DATADIR%%/lang/why3.lang +%%DATADIR%%/modules/array.mlw +%%DATADIR%%/modules/hashtbl.mlw +%%DATADIR%%/modules/impset.mlw +%%DATADIR%%/modules/mach/array.mlw +%%DATADIR%%/modules/mach/int.mlw +%%DATADIR%%/modules/matrix.mlw +%%DATADIR%%/modules/pqueue.mlw +%%DATADIR%%/modules/queue.mlw +%%DATADIR%%/modules/random.mlw +%%DATADIR%%/modules/ref.mlw +%%DATADIR%%/modules/stack.mlw +%%DATADIR%%/modules/string.mlw +%%DATADIR%%/provers-detection-data.conf +%%DATADIR%%/theories/algebra.why +%%DATADIR%%/theories/bag.why +%%DATADIR%%/theories/bintree.why +%%DATADIR%%/theories/bool.why +%%DATADIR%%/theories/comparison.why +%%DATADIR%%/theories/floating_point.why +%%DATADIR%%/theories/function.why +%%DATADIR%%/theories/graph.why +%%DATADIR%%/theories/int.why +%%DATADIR%%/theories/list.why +%%DATADIR%%/theories/map.why +%%DATADIR%%/theories/number.why +%%DATADIR%%/theories/option.why +%%DATADIR%%/theories/pigeon.why +%%DATADIR%%/theories/real.why +%%DATADIR%%/theories/regexp.why +%%DATADIR%%/theories/relations.why +%%DATADIR%%/theories/set.why +%%DATADIR%%/theories/sum.why +%%DATADIR%%/theories/tptp.why +%%DATADIR%%/vim/why3.vim +%%DATADIR%%/why3session.dtd +@dirrm %%OCAML_SITELIBDIR%%/why3 +@dirrm lib/why3/plugins +@dirrm lib/why3 +@dirrm %%DATADIR%%/drivers +@dirrm %%DATADIR%%/emacs +@dirrm %%DATADIR%%/images/boomy +@dirrm %%DATADIR%%/images/fatcow +@dirrm %%DATADIR%%/images +@dirrm %%DATADIR%%/javascript/themes/default +@dirrm %%DATADIR%%/javascript/themes +@dirrm %%DATADIR%%/javascript +@dirrm %%DATADIR%%/lang +@dirrm %%DATADIR%%/modules/mach +@dirrm %%DATADIR%%/modules +@dirrm %%DATADIR%%/theories +@dirrm %%DATADIR%%/vim +@dirrm %%DATADIR%% |