pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
(devel/why3) Updated 0.86.1 to 1.4.0, silence pkglint
Module Name: pkgsrc-wip
Committed By: Makoto Fujiwara (CF-SX3) <makoto%ki.nu@localhost>
Pushed By: mef
Date: Sat Nov 13 21:13:52 2021 +0900
Changeset: 9a47c90a3f8f5b9abc7ec5cb5c8bb79212bb0b53
Modified Files:
why3/DESCR
why3/Makefile
why3/PLIST
why3/distinfo
Log Message:
(devel/why3) Updated 0.86.1 to 1.4.0, silence pkglint
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=9a47c90a3f8f5b9abc7ec5cb5c8bb79212bb0b53
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
why3/DESCR | 17 ++--
why3/Makefile | 8 +-
why3/PLIST | 308 +++++++++++++++++++++++++++++++++-------------------------
why3/distinfo | 6 +-
4 files changed, 195 insertions(+), 144 deletions(-)
diffs:
diff --git a/why3/DESCR b/why3/DESCR
index 92452330f6..e0b64171db 100644
--- a/why3/DESCR
+++ b/why3/DESCR
@@ -1,9 +1,12 @@
-Why3 is a platform for deductive program verification. It provides a rich
+ 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
\ No newline at end of file
+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
diff --git a/why3/Makefile b/why3/Makefile
index e377e9a89a..edc7d18714 100644
--- a/why3/Makefile
+++ b/why3/Makefile
@@ -1,12 +1,12 @@
# $NetBSD: Makefile,v 1.1 2015/08/14 23:11:53 jihbed Exp $
-DISTNAME= why3-0.86.1
+DISTNAME= why3-1.4.0
CATEGORIES= devel
-MASTER_SITES= https://gforge.inria.fr/frs/download.php/file/34797/
+MASTER_SITES= https://why3.gitlabpages.inria.fr/releases/
MAINTAINER= jihbed.research%gmail.com@localhost
-HOMEPAGE= http://why3.lri.fr/#overview
-COMMENT= Why3 is a platform for deductive program verification
+HOMEPAGE= http://why3.lri.fr/
+COMMENT= Platform for deductive program verification
LICENSE= gnu-lgpl-v2.1
#DEPENDS+= frama-c-[0-9]*:../../devel/frama-c
diff --git a/why3/PLIST b/why3/PLIST
index 555c19491c..2464b59522 100644
--- a/why3/PLIST
+++ b/why3/PLIST
@@ -1,40 +1,123 @@
-@comment $NetBSD: PLIST,v 1.1 2015/08/14 23:11:53 jihbed Exp $
+@comment $NetBSD$
bin/why3
-lib/why3/commands/why3config
-lib/why3/commands/why3doc
-lib/why3/commands/why3execute
-lib/why3/commands/why3extract
-lib/why3/commands/why3prove
-lib/why3/commands/why3realize
-lib/why3/commands/why3replay
-lib/why3/commands/why3session
-lib/why3/commands/why3wc
+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/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/why3-cpulimit
+lib/why3/why3cpulimit
+lib/why3/why3server
share/emacs/site-lisp/why3.el
share/emacs/site-lisp/why3.elc
share/why3/LICENSE
share/why3/Makefile.config
share/why3/drivers/alt_ergo.drv
-share/why3/drivers/alt_ergo_0.93.drv
-share/why3/drivers/alt_ergo_0.94.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/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/cvc3_bare.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_bare.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_17_strings.drv
+share/why3/drivers/cvc4_17_strings_counterexample.drv
share/why3/drivers/cvc4_bv.gen
share/why3/drivers/discrimination.gen
share/why3/drivers/eprover.drv
@@ -42,31 +125,41 @@ 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/isabelle2018-realize.drv
+share/why3/drivers/isabelle2018.drv
+share/why3/drivers/isabelle2019-realize.drv
+share/why3/drivers/isabelle2019.drv
share/why3/drivers/mathematica.drv
share/why3/drivers/mathsat.drv
share/why3/drivers/metis.drv
share/why3/drivers/metitarski.drv
-share/why3/drivers/ocaml-gen.drv
-share/why3/drivers/ocaml-no-arith.drv
+share/why3/drivers/no-bv.gen
share/why3/drivers/ocaml-unsafe-int.drv
-share/why3/drivers/ocaml32.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.drv
+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
@@ -74,119 +167,74 @@ 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/yices_bare.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/images/boomy/accept32.png
-share/why3/images/boomy/bug32.png
-share/why3/images/boomy/clock32.png
-share/why3/images/boomy/configure16.png
-share/why3/images/boomy/configure32.png
-share/why3/images/boomy/cut32.png
-share/why3/images/boomy/cutb32.png
-share/why3/images/boomy/delete32.png
-share/why3/images/boomy/deletefile32.png
-share/why3/images/boomy/edit32.png
-share/why3/images/boomy/file16.png
-share/why3/images/boomy/file32.png
-share/why3/images/boomy/folder16.png
-share/why3/images/boomy/folder32.png
-share/why3/images/boomy/help32.png
-share/why3/images/boomy/license.txt
-share/why3/images/boomy/movefile32.png
-share/why3/images/boomy/obsaccept32.png
-share/why3/images/boomy/obsbug32.png
-share/why3/images/boomy/obsclock32.png
-share/why3/images/boomy/obsdelete32.png
-share/why3/images/boomy/obsdeletefile32.png
-share/why3/images/boomy/obshelp32.png
-share/why3/images/boomy/pause32.png
-share/why3/images/boomy/pausehalf32.png
-share/why3/images/boomy/play32.png
-share/why3/images/boomy/refresh32.png
-share/why3/images/boomy/stop32.png
-share/why3/images/boomy/transformation32.png
-share/why3/images/boomy/trashb32.png
-share/why3/images/boomy/undone32.png
-share/why3/images/boomy/wizard16.png
-share/why3/images/boomy/wizard32.png
-share/why3/images/fatcow/accept.png
-share/why3/images/fatcow/bin.png
-share/why3/images/fatcow/bomb.png
-share/why3/images/fatcow/brick_delete.png
-share/why3/images/fatcow/bullet_black.png
-share/why3/images/fatcow/bullet_blue.png
-share/why3/images/fatcow/bullet_green.png
-share/why3/images/fatcow/bullet_red.png
-share/why3/images/fatcow/bullet_white.png
-share/why3/images/fatcow/cancel.png
-share/why3/images/fatcow/control_pause_blue.png
-share/why3/images/fatcow/control_play_blue.png
-share/why3/images/fatcow/database_delete.png
-share/why3/images/fatcow/ddr_memory.png
-share/why3/images/fatcow/delete.png
-share/why3/images/fatcow/exclamation.png
-share/why3/images/fatcow/folder.png
-share/why3/images/fatcow/help.png
-share/why3/images/fatcow/magic_wand_2.png
-share/why3/images/fatcow/multitool.png
-share/why3/images/fatcow/package.png
-share/why3/images/fatcow/pencil.png
-share/why3/images/fatcow/readme-fatcow.txt
-share/why3/images/fatcow/script.png
-share/why3/images/fatcow/time_delete.png
-share/why3/images/fatcow/timeline.png
-share/why3/images/fatcow/update.png
-share/why3/images/icons.rc
-share/why3/images/logo-why.png
-share/why3/javascript/jquery.js
-share/why3/javascript/jquery.jstree.js
-share/why3/javascript/session.css
-share/why3/javascript/session.js
-share/why3/javascript/themes/default/d.gif
-share/why3/javascript/themes/default/d.png
-share/why3/javascript/themes/default/style.css
-share/why3/javascript/themes/default/throbber.gif
+share/why3/drivers/zenon_modulo.drv
share/why3/lang/why3.lang
-share/why3/modules/array.mlw
-share/why3/modules/hashtbl.mlw
-share/why3/modules/impset.mlw
-share/why3/modules/io.mlw
-share/why3/modules/mach/array.mlw
-share/why3/modules/mach/int.mlw
-share/why3/modules/mach/onetime.mlw
-share/why3/modules/mach/peano.mlw
-share/why3/modules/matrix.mlw
-share/why3/modules/null.mlw
-share/why3/modules/pqueue.mlw
-share/why3/modules/queue.mlw
-share/why3/modules/random.mlw
-share/why3/modules/ref.mlw
-share/why3/modules/stack.mlw
-share/why3/modules/string.mlw
+share/why3/lang/why3c.lang
+share/why3/lang/why3py.lang
share/why3/provers-detection-data.conf
-share/why3/theories/algebra.why
-share/why3/theories/bag.why
-share/why3/theories/bintree.why
-share/why3/theories/bool.why
-share/why3/theories/bv.why
-share/why3/theories/floating_point.why
-share/why3/theories/function.why
-share/why3/theories/graph.why
-share/why3/theories/int.why
-share/why3/theories/list.why
-share/why3/theories/map.why
-share/why3/theories/number.why
-share/why3/theories/option.why
-share/why3/theories/pigeon.why
-share/why3/theories/real.why
-share/why3/theories/regexp.why
-share/why3/theories/relations.why
-share/why3/theories/seq.why
-share/why3/theories/set.why
-share/why3/theories/sum.why
-share/why3/theories/tptp.why
-share/why3/vim/why3.vim
+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
diff --git a/why3/distinfo b/why3/distinfo
index 35f2a3cd95..2a681e6f69 100644
--- a/why3/distinfo
+++ b/why3/distinfo
@@ -1,5 +1,5 @@
$NetBSD: distinfo,v 1.1 2015/08/14 23:11:53 jihbed Exp $
-RMD160 (why3-0.86.1.tar.gz) = 57023a4d809f5783a7bea3fc956f962869fbebf3
-SHA512 (why3-0.86.1.tar.gz) = c8e0377ce2b52286cb75798b9638e0f7257f7ccf8dac901fe7410215e4dfc2efd549ab2d7b750f716b5ac0ca5f1460bb50632226a7bf09dc7e8a6d08d17c5a18
-Size (why3-0.86.1.tar.gz) = 6939963 bytes
+BLAKE2s (why3-1.4.0.tar.gz) = b636eb7ca304d9c9873fd8c76bbd3ed28ea9924b4afe6c33c3b56b419d8a9bac
+SHA512 (why3-1.4.0.tar.gz) = b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
+Size (why3-1.4.0.tar.gz) = 6306524 bytes
Home |
Main Index |
Thread Index |
Old Index