diff options
Diffstat (limited to 'math/why3')
| -rw-r--r-- | math/why3/Makefile | 22 | ||||
| -rw-r--r-- | math/why3/Makefile.common | 73 | ||||
| -rw-r--r-- | math/why3/distinfo | 2 | ||||
| -rw-r--r-- | math/why3/files/patch-src_tools_cpulimit.c | 10 | ||||
| -rw-r--r-- | math/why3/pkg-descr | 20 | ||||
| -rw-r--r-- | math/why3/pkg-plist | 204 |
6 files changed, 331 insertions, 0 deletions
diff --git a/math/why3/Makefile b/math/why3/Makefile new file mode 100644 index 000000000000..367a8d6ce23e --- /dev/null +++ b/math/why3/Makefile @@ -0,0 +1,22 @@ +# Created by: John Marino <marino@FreeBSD.org> +# $FreeBSD$ + +PORTNAME= why3 +PORTVERSION= 0.83 +CATEGORIES= math +MASTER_SITES= http://gforge.inria.fr/frs/download.php/33490/ \ + http://pkgs.fedoraproject.org/repo/pkgs/why3/${FEDORA}/ + +MAINTAINER= marino@FreeBSD.org +COMMENT= Deductive program verification platform + +LICENSE= LGPL21 + +CONFLICT_INSTALL= why3-gpl-* + +FEDORA= ${DISTNAME}${EXTRACT_SUFX}/35f99e5f64939e50ea57f641ba2073ec +ALL_TARGET= all byte +HAS_MANUAL= yes + +.include "${.CURDIR}/Makefile.common" +.include <bsd.port.mk> diff --git a/math/why3/Makefile.common b/math/why3/Makefile.common new file mode 100644 index 000000000000..2cb742ddc043 --- /dev/null +++ b/math/why3/Makefile.common @@ -0,0 +1,73 @@ +# Created by: John Marino <marino@FreeBSD.org> +# $FreeBSD$ + +BUILD_DEPENDS= ocaml-zarith>1.2:${PORTSDIR}/math/ocaml-zarith \ + lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 \ + ocaml-sqlite3>2:${PORTSDIR}/databases/ocaml-sqlite3 \ + ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph \ + camlp5o:${PORTSDIR}/devel/ocaml-camlp5 + +GNU_CONFIGURE= yes +INSTALL_TARGET= install-all + +USES= gmake +USE_OCAML= yes +MAKE_JOBS_UNSAFE= yes + +# The FRAMA_C plugin is experimental, it actually doesn't even build +# with ocaml 4.01. Leave the option commented out for future use. +# There is something wrong with coq, it rebuilds itself in /usr/local. +# Leave it for now with a TO-DO to fix coq +# Isabelle is currently i386-only due to issues with polyml and default +# reliance on i386-only sml-nj (also currently broke). Disable for now. + +CONFIGURE_ARGS= --enable-relocation \ + --disable-doc \ + --disable-pvs-libs \ + --disable-profiling \ + --disable-coq-tactic \ + --disable-coq-libs \ + --disable-isabelle-libs + +.if defined(HAS_MANUAL) +PORTDOCS= manual.pdf +OPTIONS_DEFINE= DOCS #ISABELLE COQ FRAMA_C +.endif + +COQ_CONFIGURE_ENABLE= coq-tactic coq-libs +COQ_DESC= Build coq realizations and tactics +COQ_BUILD_DEPENDS= coqc:${PORTSDIR}/math/coq +COQ_RUN_DEPENDS= coqc:${PORTSDIR}/math/coq +FRAMA_C_CONFIGURE_ENABLE= frama_c +FRAMA_C_DESC= Build Frama-C plugin +FRAMA_C_BUILD_DEPENDS= frama-c:${PORTSDIR}/devel/frama-c +FRAMA_C_RUN_DEPENDS= frama-c:${PORTSDIR}/devel/frama-c +ISABELLE_CONFIGURE_ENABLE= isabelle-libs +ISABELLE_DESC= Enable Isabelle realizations +ISABELLE_BUILD_DEPENDS= isabelle:${PORTSDIR}/math/isabelle +ISABELLE_RUN_DEPENDS= isabelle:${PORTSDIR}/math/isabelle + +# The pdf is pre-built, but the makefile wants to build it again in order +# to generate manual.bbl which is used to build the html documention. +# Regenerating pdf fails, and the dependencies are heavy. Disable this +# all for now and just manually install the pdf. The "doc" target was +# also removed from ALL_TARGET +# +#DOCS_CONFIGURE_ENABLE= doc +#DOCS_BUILD_DEPENDS= rubber:${PORTSDIR}/textproc/rubber \ +# hevea:${PORTSDIR}/textproc/hevea + +.include <bsd.port.options.mk> + +post-patch: + @${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \ + ${WRKSRC}/src/util/sysutil.ml \ + ${WRKSRC}/src/jessie/Makefile.in + +post-install: +.if ${PORT_OPTIONS:MDOCS} +. if defined(HAS_MANUAL) + ${MKDIR} ${STAGEDIR}${DOCSDIR} + ${INSTALL_DATA} ${WRKSRC}/doc/manual.pdf ${STAGEDIR}${DOCSDIR} +. endif +.endif diff --git a/math/why3/distinfo b/math/why3/distinfo new file mode 100644 index 000000000000..2c961b8aba61 --- /dev/null +++ b/math/why3/distinfo @@ -0,0 +1,2 @@ +SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9 +SIZE (why3-0.83.tar.gz) = 5347628 diff --git a/math/why3/files/patch-src_tools_cpulimit.c b/math/why3/files/patch-src_tools_cpulimit.c new file mode 100644 index 000000000000..5c905ece014a --- /dev/null +++ b/math/why3/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/pkg-descr b/math/why3/pkg-descr new file mode 100644 index 000000000000..ed0b7f1fea9c --- /dev/null +++ b/math/why3/pkg-descr @@ -0,0 +1,20 @@ +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. + +WWW: http://why3.lri.fr diff --git a/math/why3/pkg-plist b/math/why3/pkg-plist new file mode 100644 index 000000000000..f59dd690d4a1 --- /dev/null +++ b/math/why3/pkg-plist @@ -0,0 +1,204 @@ +bin/why3 +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.cma +%%OCAML_SITELIBDIR%%/why3/why3.cmi +%%OCAML_SITELIBDIR%%/why3/why3.cmo +%%OCAML_SITELIBDIR%%/why3/why3.cmx +%%OCAML_SITELIBDIR%%/why3/why3.cmxa +%%OCAML_SITELIBDIR%%/why3/why3.o +%%OCAML_SITELIBDIR%%/why3/why3extract.a +%%OCAML_SITELIBDIR%%/why3/why3extract.cma +%%OCAML_SITELIBDIR%%/why3/why3extract.cmi +%%OCAML_SITELIBDIR%%/why3/why3extract.cmo +%%OCAML_SITELIBDIR%%/why3/why3extract.cmx +%%OCAML_SITELIBDIR%%/why3/why3extract.cmxa +%%OCAML_SITELIBDIR%%/why3/why3extract.o +lib/why3/plugins/dimacs.cmo +lib/why3/plugins/dimacs.cmxs +lib/why3/plugins/genequlin.cmo +lib/why3/plugins/genequlin.cmxs +lib/why3/plugins/hypothesis_selection.cmo +lib/why3/plugins/hypothesis_selection.cmxs +lib/why3/plugins/tptp.cmo +lib/why3/plugins/tptp.cmxs +lib/why3/why3-call-pvs +lib/why3/why3-cpulimit +%%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/cvc3.drv +%%DATADIR%%/drivers/cvc3_bare.drv +%%DATADIR%%/drivers/cvc4.drv +%%DATADIR%%/drivers/cvc4_bare.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.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%% |