CVS commit: pkgsrc/devel/why3

To: pkgsrc-changes%NetBSD.org@localhost
Subject: CVS commit: pkgsrc/devel/why3
From: "Antoine Reilles" <tonio%netbsd.org@localhost>
Date: Sat, 8 Oct 2022 16:36:47 +0000

Module Name:    pkgsrc
Committed By:   tonio
Date:           Sat Oct  8 16:36:47 UTC 2022

Added Files:
        pkgsrc/devel/why3: DESCR Makefile PLIST distinfo

Log Message:
Adding devel/why3 1.5.1

Import from WIP, thanks jihbed.research%gmail.com@localhost

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.


To generate a diff of this commit:
cvs rdiff -u -r0 -r1.1 pkgsrc/devel/why3/DESCR pkgsrc/devel/why3/Makefile \
    pkgsrc/devel/why3/PLIST pkgsrc/devel/why3/distinfo

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Added files:

Index: pkgsrc/devel/why3/DESCR
diff -u /dev/null pkgsrc/devel/why3/DESCR:1.1
--- /dev/null   Sat Oct  8 16:36:47 2022
+++ pkgsrc/devel/why3/DESCR     Sat Oct  8 16:36:47 2022
@@ -0,0 +1,12 @@
+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.
Index: pkgsrc/devel/why3/Makefile
diff -u /dev/null pkgsrc/devel/why3/Makefile:1.1
--- /dev/null   Sat Oct  8 16:36:47 2022
+++ pkgsrc/devel/why3/Makefile  Sat Oct  8 16:36:47 2022
@@ -0,0 +1,20 @@
+# $NetBSD: Makefile,v 1.1 2022/10/08 16:36:47 tonio Exp $
+
+DISTNAME=      why3-1.5.1
+CATEGORIES=    devel
+MASTER_SITES=  https://why3.gitlabpages.inria.fr/releases/
+
+MAINTAINER=    jihbed.research%gmail.com@localhost
+HOMEPAGE=      http://why3.lri.fr/
+COMMENT=       Platform for deductive program verification
+LICENSE=       gnu-lgpl-v2.1
+
+DEPENDS+=      menhir-[0-9]*:../../devel/menhir
+
+GNU_CONFIGURE= yes
+USE_TOOLS+=    gmake
+
+CONFIGURE_ARGS+=               --disable-ide
+
+.include "../../lang/ocaml/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/devel/why3/PLIST
diff -u /dev/null pkgsrc/devel/why3/PLIST:1.1
--- /dev/null   Sat Oct  8 16:36:47 2022
+++ pkgsrc/devel/why3/PLIST     Sat Oct  8 16:36:47 2022
@@ -0,0 +1,241 @@
+@comment $NetBSD: PLIST,v 1.1 2022/10/08 16:36:47 tonio Exp $
+bin/isabelle_client
+bin/why3
+lib/why3/commands/why3config.cmxs
+lib/why3/commands/why3doc.cmxs
+lib/why3/commands/why3execute.cmxs
+lib/why3/commands/why3extract.cmxs
+lib/why3/commands/why3pp.cmxs
+lib/why3/commands/why3prove.cmxs
+lib/why3/commands/why3realize.cmxs
+lib/why3/commands/why3replay.cmxs
+lib/why3/commands/why3session.cmxs
+lib/why3/commands/why3shell.cmxs
+lib/why3/commands/why3show.cmxs
+lib/why3/commands/why3wc.cmxs
+lib/why3/commands/why3webserver.cmxs
+lib/why3/coq/BuiltIn.vo
+lib/why3/coq/HighOrd.vo
+lib/why3/coq/bool/Bool.vo
+lib/why3/coq/bv/BV_Gen.vo
+lib/why3/coq/bv/Pow2int.vo
+lib/why3/coq/for_drivers/ComputerOfEuclideanDivision.vo
+lib/why3/coq/int/Abs.vo
+lib/why3/coq/int/ComputerDivision.vo
+lib/why3/coq/int/Div2.vo
+lib/why3/coq/int/EuclideanDivision.vo
+lib/why3/coq/int/Exponentiation.vo
+lib/why3/coq/int/Int.vo
+lib/why3/coq/int/MinMax.vo
+lib/why3/coq/int/NumOf.vo
+lib/why3/coq/int/Power.vo
+lib/why3/coq/list/Append.vo
+lib/why3/coq/list/Combine.vo
+lib/why3/coq/list/Distinct.vo
+lib/why3/coq/list/HdTl.vo
+lib/why3/coq/list/HdTlNoOpt.vo
+lib/why3/coq/list/Length.vo
+lib/why3/coq/list/List.vo
+lib/why3/coq/list/Mem.vo
+lib/why3/coq/list/Nth.vo
+lib/why3/coq/list/NthHdTl.vo
+lib/why3/coq/list/NthLength.vo
+lib/why3/coq/list/NthLengthAppend.vo
+lib/why3/coq/list/NthNoOpt.vo
+lib/why3/coq/list/NumOcc.vo
+lib/why3/coq/list/Permut.vo
+lib/why3/coq/list/RevAppend.vo
+lib/why3/coq/list/Reverse.vo
+lib/why3/coq/map/Const.vo
+lib/why3/coq/map/Map.vo
+lib/why3/coq/map/MapInjection.vo
+lib/why3/coq/map/MapPermut.vo
+lib/why3/coq/map/Occ.vo
+lib/why3/coq/number/Coprime.vo
+lib/why3/coq/number/Divisibility.vo
+lib/why3/coq/number/Gcd.vo
+lib/why3/coq/number/Parity.vo
+lib/why3/coq/number/Prime.vo
+lib/why3/coq/option/Option.vo
+lib/why3/coq/real/Abs.vo
+lib/why3/coq/real/ExpLog.vo
+lib/why3/coq/real/FromInt.vo
+lib/why3/coq/real/MinMax.vo
+lib/why3/coq/real/PowerInt.vo
+lib/why3/coq/real/PowerReal.vo
+lib/why3/coq/real/Real.vo
+lib/why3/coq/real/RealInfix.vo
+lib/why3/coq/real/Square.vo
+lib/why3/coq/real/Trigonometry.vo
+lib/why3/coq/set/Cardinal.vo
+lib/why3/coq/set/Fset.vo
+lib/why3/coq/set/FsetInduction.vo
+lib/why3/coq/set/FsetInt.vo
+lib/why3/coq/set/FsetSum.vo
+lib/why3/coq/set/Set.vo
+lib/why3/coq/set/SetApp.vo
+lib/why3/coq/set/SetAppInt.vo
+lib/why3/coq/set/SetImp.vo
+lib/why3/coq/set/SetImpInt.vo
+lib/why3/coq/version
+lib/why3/plugins/cfg.cmxs
+lib/why3/plugins/dimacs.cmxs
+lib/why3/plugins/genequlin.cmxs
+lib/why3/plugins/hypothesis_selection.cmxs
+lib/why3/plugins/microc.cmxs
+lib/why3/plugins/python.cmxs
+lib/why3/plugins/tptp.cmxs
+lib/why3/why3-call-pvs
+lib/why3/why3cpulimit
+lib/why3/why3server
+share/emacs/site-lisp/why3.el
+share/why3/LICENSE
+share/why3/Makefile.config
+share/why3/drivers/alt_ergo.drv
+share/why3/drivers/alt_ergo_2_2_0.drv
+share/why3/drivers/alt_ergo_2_3.drv
+share/why3/drivers/alt_ergo_common.drv
+share/why3/drivers/alt_ergo_fp.drv
+share/why3/drivers/alt_ergo_model.drv
+share/why3/drivers/alt_ergo_smt2.drv
+share/why3/drivers/beagle.drv
+share/why3/drivers/c.drv
+share/why3/drivers/cakeml.drv
+share/why3/drivers/colibri.drv
+share/why3/drivers/colibri2.drv
+share/why3/drivers/coq-common.gen
+share/why3/drivers/coq-realizations.aux
+share/why3/drivers/coq-realize.drv
+share/why3/drivers/coq-ssreflect.drv
+share/why3/drivers/coq.drv
+share/why3/drivers/cvc3.drv
+share/why3/drivers/cvc4-realize.drv
+share/why3/drivers/cvc4.drv
+share/why3/drivers/cvc4_14.drv
+share/why3/drivers/cvc4_15.drv
+share/why3/drivers/cvc4_15_counterexample.drv
+share/why3/drivers/cvc4_16.drv
+share/why3/drivers/cvc4_16.gen
+share/why3/drivers/cvc4_16_counterexample.drv
+share/why3/drivers/cvc4_17.drv
+share/why3/drivers/cvc4_17_counterexample.drv
+share/why3/drivers/cvc4_18_strings.drv
+share/why3/drivers/cvc4_18_strings_counterexample.drv
+share/why3/drivers/cvc4_bv.gen
+share/why3/drivers/discrimination.gen
+share/why3/drivers/eprover.drv
+share/why3/drivers/gappa.drv
+share/why3/drivers/iprover.drv
+share/why3/drivers/isabelle-common.gen
+share/why3/drivers/isabelle-realizations.aux
+share/why3/drivers/isabelle-realize.drv
+share/why3/drivers/isabelle.drv
+share/why3/drivers/mathematica.drv
+share/why3/drivers/mathsat.drv
+share/why3/drivers/metis.drv
+share/why3/drivers/metitarski.drv
+share/why3/drivers/no-bv.gen
+share/why3/drivers/ocaml-unsafe-int.drv
+share/why3/drivers/ocaml64.drv
+share/why3/drivers/polypaver.drv
+share/why3/drivers/princess.drv
+share/why3/drivers/psyche.drv
+share/why3/drivers/pvs-common.gen
+share/why3/drivers/pvs-realizations.aux
+share/why3/drivers/pvs-realize.drv
+share/why3/drivers/pvs.drv
+share/why3/drivers/safeprover.drv
+share/why3/drivers/simplify.drv
+share/why3/drivers/smt-libv2-bv-realization.gen
+share/why3/drivers/smt-libv2-bv.gen
+share/why3/drivers/smt-libv2-floats-gnatprove.gen
+share/why3/drivers/smt-libv2-floats-int_via_bv.gen
+share/why3/drivers/smt-libv2-floats-int_via_real.gen
+share/why3/drivers/smt-libv2-floats.gen
+share/why3/drivers/smt-libv2-gnatprove.gen
+share/why3/drivers/smt-libv2.gen
+share/why3/drivers/smtlib-strings.gen
+share/why3/drivers/spass.drv
+share/why3/drivers/spass_types.drv
+share/why3/drivers/tptp-tff0.drv
+share/why3/drivers/tptp-tff1.drv
+share/why3/drivers/tptp.gen
+share/why3/drivers/vampire-smt.drv
+share/why3/drivers/vampire.drv
+share/why3/drivers/verit.drv
+share/why3/drivers/why3.drv
+share/why3/drivers/why3_smt.drv
+share/why3/drivers/why3_tptp.drv
+share/why3/drivers/yices-smt2.drv
+share/why3/drivers/yices.drv
+share/why3/drivers/z3.drv
+share/why3/drivers/z3_432.drv
+share/why3/drivers/z3_440.drv
+share/why3/drivers/z3_440_counterexample.drv
+share/why3/drivers/z3_471.drv
+share/why3/drivers/z3_471_counterexample.drv
+share/why3/drivers/z3_471_nobv.drv
+share/why3/drivers/z3_bv.gen
+share/why3/drivers/z3_smtv1.drv
+share/why3/drivers/zenon.drv
+share/why3/drivers/zenon_modulo.drv
+share/why3/lang/why3.lang
+share/why3/lang/why3c.lang
+share/why3/lang/why3py.lang
+share/why3/provers-detection-data.conf
+share/why3/stdlib/algebra.mlw
+share/why3/stdlib/array.mlw
+share/why3/stdlib/bag.mlw
+share/why3/stdlib/bintree.mlw
+share/why3/stdlib/bool.mlw
+share/why3/stdlib/bv.mlw
+share/why3/stdlib/byte_string.mlw
+share/why3/stdlib/cursor.mlw
+share/why3/stdlib/debug.mlw
+share/why3/stdlib/exn.mlw
+share/why3/stdlib/floating_point.mlw
+share/why3/stdlib/fmap.mlw
+share/why3/stdlib/for_drivers.mlw
+share/why3/stdlib/function.mlw
+share/why3/stdlib/graph.mlw
+share/why3/stdlib/hashtbl.mlw
+share/why3/stdlib/ieee_float.mlw
+share/why3/stdlib/int.mlw
+share/why3/stdlib/io.mlw
+share/why3/stdlib/list.mlw
+share/why3/stdlib/mach/array.mlw
+share/why3/stdlib/mach/bv.mlw
+share/why3/stdlib/mach/c.mlw
+share/why3/stdlib/mach/float.mlw
+share/why3/stdlib/mach/fxp.mlw
+share/why3/stdlib/mach/int.mlw
+share/why3/stdlib/mach/matrix.mlw
+share/why3/stdlib/mach/onetime.mlw
+share/why3/stdlib/mach/peano.mlw
+share/why3/stdlib/mach/tagset.mlw
+share/why3/stdlib/map.mlw
+share/why3/stdlib/matrix.mlw
+share/why3/stdlib/microc.mlw
+share/why3/stdlib/null.mlw
+share/why3/stdlib/number.mlw
+share/why3/stdlib/ocaml.mlw
+share/why3/stdlib/option.mlw
+share/why3/stdlib/pigeon.mlw
+share/why3/stdlib/pqueue.mlw
+share/why3/stdlib/python.mlw
+share/why3/stdlib/queue.mlw
+share/why3/stdlib/random.mlw
+share/why3/stdlib/real.mlw
+share/why3/stdlib/ref.mlw
+share/why3/stdlib/regexp.mlw
+share/why3/stdlib/relations.mlw
+share/why3/stdlib/seq.mlw
+share/why3/stdlib/set.mlw
+share/why3/stdlib/stack.mlw
+share/why3/stdlib/string.mlw
+share/why3/stdlib/tptp.mlw
+share/why3/stdlib/tree.mlw
+share/why3/stdlib/witness.mlw
+share/why3/vim/ftdetect/why3.vim
+share/why3/vim/syntax/why3.vim
+share/why3/why3session.dtd
Index: pkgsrc/devel/why3/distinfo
diff -u /dev/null pkgsrc/devel/why3/distinfo:1.1
--- /dev/null   Sat Oct  8 16:36:47 2022
+++ pkgsrc/devel/why3/distinfo  Sat Oct  8 16:36:47 2022
@@ -0,0 +1,5 @@
+$NetBSD: distinfo,v 1.1 2022/10/08 16:36:47 tonio Exp $
+
+BLAKE2s (why3-1.5.1.tar.gz) = c4be800397c011a99d13526488d56aae4ff5c260ddff5a1ac843149145e6a855
+SHA512 (why3-1.5.1.tar.gz) = 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
+Size (why3-1.5.1.tar.gz) = 6727576 bytes

Prev by Date: CVS commit: pkgsrc/doc
Next by Date: CVS commit: pkgsrc/devel
Previous by Thread: CVS commit: pkgsrc/doc
Next by Thread: CVS commit: pkgsrc/devel
Indexes:

Home | Main Index | Thread Index | Old Index