Received: by mail.netbsd.org (Postfix, from userid 605) id 9C1D684D91; Sat, 8 Oct 2022 16:36:49 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by mail.netbsd.org (Postfix) with ESMTP id CBD4684D5F for ; Sat, 8 Oct 2022 16:36:48 +0000 (UTC) X-Virus-Scanned: amavisd-new at netbsd.org Received: from mail.netbsd.org ([127.0.0.1]) by localhost (mail.netbsd.org [127.0.0.1]) (amavisd-new, port 10025) with ESMTP id jKlMwATj_X_a for ; Sat, 8 Oct 2022 16:36:47 +0000 (UTC) Received: from cvs.NetBSD.org (ivanova.NetBSD.org [IPv6:2001:470:a085:999:28c:faff:fe03:5984]) by mail.netbsd.org (Postfix) with ESMTP id AA1F884CE8 for ; Sat, 8 Oct 2022 16:36:47 +0000 (UTC) Received: by cvs.NetBSD.org (Postfix, from userid 500) id 9DF4DFA90; Sat, 8 Oct 2022 16:36:47 +0000 (UTC) Content-Transfer-Encoding: 7bit Content-Type: multipart/mixed; boundary="_----------=_1665247007235510" MIME-Version: 1.0 Date: Sat, 8 Oct 2022 16:36:47 +0000 From: "Antoine Reilles" Subject: CVS commit: pkgsrc/devel/why3 To: pkgsrc-changes@NetBSD.org Reply-To: tonio@netbsd.org X-Mailer: log_accum Message-Id: <20221008163647.9DF4DFA90@cvs.NetBSD.org> Sender: pkgsrc-changes-owner@NetBSD.org List-Id: Precedence: bulk List-Unsubscribe: This is a multi-part message in MIME format. --_----------=_1665247007235510 Content-Disposition: inline Content-Transfer-Encoding: 8bit Content-Type: text/plain; charset="US-ASCII" 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 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. --_----------=_1665247007235510 Content-Disposition: inline Content-Length: 10125 Content-Transfer-Encoding: binary Content-Type: text/x-diff; charset=us-ascii 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 +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 --_----------=_1665247007235510--