CVS commit: pkgsrc/devel/why3

To: pkgsrc-changes%NetBSD.org@localhost
Subject: CVS commit: pkgsrc/devel/why3
From: "David A. Holland" <dholland%netbsd.org@localhost>
Date: Mon, 3 Mar 2025 03:27:05 +0000

Module Name:    pkgsrc
Committed By:   dholland
Date:           Mon Mar  3 03:27:05 UTC 2025

Modified Files:
        pkgsrc/devel/why3: Makefile PLIST distinfo

Log Message:
devel/why3: update to 1.8.0 to fix build with current Coq

pkgsrc changes:
   - update homepage
   - update minimum coq version
   - ocaml-num -> ocaml-zarith
   - enable the GUI since lablgtk3 must be present anyway for coq

Upstream changelog:

:x: marks a potential source of incompatibility

Version 1.8.0, December 11, 2024
--------------------------------

Standard library
  * new library `ufloat`: unbounded floating-point numbers
  * new library `coma`: standard library of the plugin Coma
  * additional operators in library `fmap`
  * added 16-bit integers in `mach/int`
  * added a program equality in `bool`
  * added meta annotations for "unused dependencies", which usually
    improve proof automation but very rarely may lose some proofs :x:
  * made most `(==)` operators trigger the `extensionality` transformation :x:

Core
  * records and range types now have some predefined symbol `foo'eq`
    and some axiom `foo'inj` to express injectivity. See manual
    Section "The WhyML Language Reference/Record Types".

Transformations
  * new transformation `extensionality` to help with equality proofs

Plugins
  * new task-oriented strategy `forward_propagation` to automatically
    propagate rounding errors
  * new frontend plugin "Coma"

Provers
  * Alt-Ergo FPA requires Alt-Ergo >= 2.5.4
  * drop support for versions of Coq < 8.16
  * support for Coq 8.19 (released Jan 24, 2024)
  * support for Z3 4.13 (released Mar 7, 2024)
  * support for CVC5 1.2 (released Aug 8, 2024)
  * support for Coq 8.20 (released Sep 11, 2024)
  * support for Alt-Ergo 2.6 (released Sep 24, 2024)

Tools
  * `why3 prove`: dropped option `--json-model-values` :x:
  * `why3 execute`: added option `--rac-memlimit`;
    the `--rac-prover` option no longer supports specifying a time limit
    and memory limit :x:
  * `why3 pp`: the LaTeX output now shows algebraic types and logic definitions
  * `why3 pp`: dropped option `--kind` :x:

Extraction
  * added support for Java, see Manual, Section "Executing WhyML Programs"
  * improved extraction to C: floating-point numbers, global variables

API
  * changed how resource limits are specified :x
  * renamed type `effect` to `effekt` for compatibility with OCaml 5.3 :x

Miscellaneous
  * dependency on OCaml library `num` was replaced by `zarith`

Version 1.7.2, April 18, 2024
-----------------------------

Bug fixes
  * restored the legacy shortcut for Alt-Ergo 2.5
  * fixed various bugs in the lexer of `why3 doc`
  * made prover detection more reliable when paths need escaping

Version 1.7.1, January 20, 2024
-------------------------------

Bug fixes
  * restored syntax highlighting in IDE
  * improved detection of Isabelle 2022 and Alt-Ergo 2.5

Version 1.7.0, November 24, 2023
--------------------------------

WhyML language
  * syntax `module Impl: Intf ... end` can be used to hide the
    details of an implementation during proofs

MLCFG language
  * `variant` clauses are supported with the `stackify` backend
  * `invariant` names are now optional and deprecated

Input formats
  * a new input format `.sexp` is supported for programs written as
    S-expressions; this input format, intended as an intermediate language,
    is compatible with the output of `why3 pp --output=sexp` and
    the S-expressions generated by the API function `Ptree.sexp_of_mlw_file`

Standard library
  * library `ieee_float`: added conversions between floating-point numbers
    and signed bitvectors, with appropriate mappings to SMT-LIB

IDE
  * strategies can now execute a group of provers concurrently in a single
    `call` step, by separating provers by a `|`; default strategies now
    make use of this parallelism for time limits larger than 1 second

Tools
  * option `--warn-off=...` can now be used to disable individual warnings;
    available warnings can be listed using `--list-warning-flags`
  * driver files appearing in a configuration file loaded using option
    `--extra-config` are now also searched in the sub-directory of that
    configuration file
  * `why3 session info` now produces separate statistics per session
    and overall statistics; see Section 5.5.1 of the manual :x:
  * `why3 session update` now supports options `--mark-obsolete`,
    `--remove-proofs`, and `--add-provers`, together with selection of proof
    nodes via filters; see Section 5.5.4 of the manual
  * `why3 session create` now generates a new session for the specified files;
    see Section 5.5.5 of the manual
  * `why3 session info` now has an option `--graph=[all|hist|scatter]`;
    `all` corresponds to the old behavior, while `hist` and `scatter` provide
    finer graphs for pairwise comparison of provers
  * `why3 bench` now provides a way to run all the proof attempts that
    have not been run before; see Section 5.13 of the manual
  * `why3 replay` now supports option `--ignore-shapes`, which disables the use
    of shapes when merging sessions
  * time taken by solvers is now uniformly reported with the precision
    of a microsecond, in particular in session files; cumulative times,
    e.g., reported by `why3 session info --provers-stats`, are more precise;
    the `time` regexp in driver files is deprecated and the time taken by
    solvers is now measured by Why3 directly

Provers
  * support for Coq 8.17.0 (released Mar 23, 2023)
  * support for Coq 8.18.0 (released Sep 7, 2023)
  * drop support for versions of Coq < 8.11
  * support for Alt-Ergo 2.4.3
  * support for Alt-Ergo 2.5.x with SMT syntax and counterexamples
  * support for Z3 4.12.x
  * support for CVC5 1.0.5

Miscellaneous
  * configuration option `--disable-pp-sexp` has been renamed into `--disable-sexp` :x:
  * debug flag `ignore_missing_diverges` has been renamed into `missing_diverges` :x:
  * debug flag `ignore_unused_vars` has been renamed into `unused_variable` :x:
  * debug flag `stats` now also records the time taken by transformations

Version 1.6.0, March 7, 2023
----------------------------

Core
  * added meta `vc:proved_wf` for annotating well-founded relations, to make
    them easier to use in variants; see Section 8.2.3 of the manual

Standard library
  * relations `ult`, `ugt`, `slt`, and `sgt` from `bv` modules are now
    recognized as well-founded

Tools
  * `libdir` and `datadir` are not stored anymore in the configuration file,
    but they can still be manually set there if needed;
    see also the environment variables `WHY3LIB` and `WHY3DATA`
  * several debug flags have been renamed;
    use `why3 --list-debug-flags` to obtain the new names :x:
  * global directives in extra drivers are now taken into account
  * time limits now have a sub-second accuracy, e.g., `--timelimit=0.5`

IDE
  * pressing Tab now auto-completes commands
  * added menu item "File/Export as Zip" to export a zip archive of the
    current session and all the related files

Web interface TryWhy3
  * proof obligations are now displayed as a sequent rather than a full task

Python language
  * added `by` and `so` connectives in predicates
  * fixed overloading of `+` in Python code
  * added `add_list` for list concatenation in logic

MLCFG language
  * attributes on function bodies are now supported
  * attributes `[@cfg:stackify]` and `[@cfg:subregion_analysis]` can
    be used to improve the VC structure and generate extra invariants;
    see Sections 7.3.5 and 7.3.6 of the manual

API
  * source locations now use both a starting line and an ending line;
    the fourth number is thus the column on the last line :x:
  * several functions from `Call_prover` and `Driver` now take as input a
    `Whyconf.main` configuration type instead of directly taking `libdir`
    and `datadir` :x:
  * `Whyconf.load_driver` has been replaced by `Driver.load_driver_for_prover` :x:
  * `Warning.emit` has been replaced by `Loc.warning` :x:
  * representation of counterexamples has been modified;
    see Sections 5.3.7.1, 11.10.3, and 12.11 of the manual

Provers
  * support for CVC5 1.0.0 to 1.0.4 (released Jan 31, 2023)
  * support for Alt-Ergo 2.4.2 (released Aug 1, 2022)
  * support for Z3 4.12.0 and 4.12.1 (released Jan 18, 2023)
  * support for Isabelle 2022 (released Oct 2022)

Miscellaneous
  * fixed soundness bug with existential quantifiers in `introduce_premises`
  * configuration option `--enable-profiling` has been removed
  * configuration now fails for explicit yet unsuccessful `--enable-foo` options
  * OCaml >= 4.08 is now required
  * LablGtk2 is no longer supported


To generate a diff of this commit:
cvs rdiff -u -r1.5 -r1.6 pkgsrc/devel/why3/Makefile
cvs rdiff -u -r1.2 -r1.3 pkgsrc/devel/why3/PLIST
cvs rdiff -u -r1.1 -r1.2 pkgsrc/devel/why3/distinfo

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

Modified files:

Index: pkgsrc/devel/why3/Makefile
diff -u pkgsrc/devel/why3/Makefile:1.5 pkgsrc/devel/why3/Makefile:1.6
--- pkgsrc/devel/why3/Makefile:1.5      Sun Oct 16 10:51:45 2022
+++ pkgsrc/devel/why3/Makefile  Mon Mar  3 03:27:04 2025
@@ -1,7 +1,6 @@
-# $NetBSD: Makefile,v 1.5 2022/10/16 10:51:45 tonio Exp $
+# $NetBSD: Makefile,v 1.6 2025/03/03 03:27:04 dholland Exp $
 
-DISTNAME=      why3-1.5.1
-PKGREVISION=   1
+DISTNAME=      why3-1.8.0
 CATEGORIES=    devel
 MASTER_SITES=  https://why3.gitlabpages.inria.fr/releases/
 
@@ -15,12 +14,12 @@ DEPENDS+=   menhir-[0-9]*:../../devel/menh
 GNU_CONFIGURE= yes
 USE_TOOLS+=    gmake
 
-CONFIGURE_ARGS+=       --disable-ide
 INSTALL_TARGET=                install install-lib
 
-DEPENDS+=              coq>=8.6:../../lang/coq
+DEPENDS+=              coq>=8.16:../../lang/coq
 
 .include "../../lang/ocaml/buildlink3.mk"
 .include "../../devel/ocamlgraph/buildlink3.mk"
-.include "../../math/ocaml-num/buildlink3.mk"
+.include "../../math/ocaml-zarith/buildlink3.mk"
+.include "../../x11/ocaml-lablgtk3/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"

Index: pkgsrc/devel/why3/PLIST
diff -u pkgsrc/devel/why3/PLIST:1.2 pkgsrc/devel/why3/PLIST:1.3
--- pkgsrc/devel/why3/PLIST:1.2 Sun Oct  9 06:46:57 2022
+++ pkgsrc/devel/why3/PLIST     Mon Mar  3 03:27:04 2025
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.2 2022/10/09 06:46:57 tonio Exp $
+@comment $NetBSD: PLIST,v 1.3 2025/03/03 03:27:04 dholland Exp $
 bin/isabelle_client
 bin/why3
 lib/ocaml/site-lib/why3/META
@@ -8,10 +8,12 @@ lib/ocaml/site-lib/why3/why3.cmt
 lib/ocaml/site-lib/why3/why3.cmx
 lib/ocaml/site-lib/why3/why3.cmxa
 lib/ocaml/site-lib/why3/why3.cmxs
+lib/why3/commands/why3bench.cmxs
 lib/why3/commands/why3config.cmxs
 lib/why3/commands/why3doc.cmxs
 lib/why3/commands/why3execute.cmxs
 lib/why3/commands/why3extract.cmxs
+lib/why3/commands/why3ide.cmxs
 lib/why3/commands/why3pp.cmxs
 lib/why3/commands/why3prove.cmxs
 lib/why3/commands/why3realize.cmxs
@@ -23,6 +25,7 @@ lib/why3/commands/why3wc.cmxs
 lib/why3/commands/why3webserver.cmxs
 lib/why3/coq/BuiltIn.vo
 lib/why3/coq/HighOrd.vo
+lib/why3/coq/WellFounded.vo
 lib/why3/coq/bool/Bool.vo
 lib/why3/coq/bv/BV_Gen.vo
 lib/why3/coq/bv/Pow2int.vo
@@ -55,6 +58,7 @@ 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/MapExt.vo
 lib/why3/coq/map/MapInjection.vo
 lib/why3/coq/map/MapPermut.vo
 lib/why3/coq/map/Occ.vo
@@ -86,7 +90,9 @@ lib/why3/coq/set/SetImp.vo
 lib/why3/coq/set/SetImpInt.vo
 lib/why3/coq/version
 lib/why3/plugins/cfg.cmxs
+lib/why3/plugins/coma.cmxs
 lib/why3/plugins/dimacs.cmxs
+lib/why3/plugins/forward_propagation.cmxs
 lib/why3/plugins/genequlin.cmxs
 lib/why3/plugins/hypothesis_selection.cmxs
 lib/why3/plugins/microc.cmxs
@@ -96,20 +102,24 @@ lib/why3/why3-call-pvs
 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_26.drv
+share/why3/drivers/alt_ergo_26_bv.drv
+share/why3/drivers/alt_ergo_26_ce.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_counterexamples.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/alt_ergo_smt.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/common-transformations.gen
 share/why3/drivers/coq-common.gen
 share/why3/drivers/coq-realizations.aux
 share/why3/drivers/coq-realize.drv
@@ -129,7 +139,12 @@ share/why3/drivers/cvc4_17_counterexampl
 share/why3/drivers/cvc4_18_strings.drv
 share/why3/drivers/cvc4_18_strings_counterexample.drv
 share/why3/drivers/cvc4_bv.gen
+share/why3/drivers/cvc5.drv
+share/why3/drivers/cvc5_counterexample.drv
+share/why3/drivers/cvc5_strings.drv
+share/why3/drivers/cvc5_strings_counterexample.drv
 share/why3/drivers/discrimination.gen
+share/why3/drivers/dreal.drv
 share/why3/drivers/eprover.drv
 share/why3/drivers/gappa.drv
 share/why3/drivers/iprover.drv
@@ -142,8 +157,6 @@ 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
@@ -155,11 +168,7 @@ 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
@@ -167,8 +176,9 @@ 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/vampire_4_2_2.drv
+share/why3/drivers/vampire_4_5_1.drv
 share/why3/drivers/verit.drv
 share/why3/drivers/why3.drv
 share/why3/drivers/why3_smt.drv
@@ -182,10 +192,46 @@ share/why3/drivers/z3_440_counterexample
 share/why3/drivers/z3_471.drv
 share/why3/drivers/z3_471_counterexample.drv
 share/why3/drivers/z3_471_nobv.drv
+share/why3/drivers/z3_487.drv
+share/why3/drivers/z3_487_counterexample.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/extraction_drivers/c.drv
+share/why3/extraction_drivers/cakeml.drv
+share/why3/extraction_drivers/java.drv
+share/why3/extraction_drivers/ocaml64.drv
+share/why3/images/fatcow.rc
+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/logo-why.png
+share/why3/lang/coma.lang
 share/why3/lang/why3.lang
 share/why3/lang/why3c.lang
 share/why3/lang/why3py.lang
@@ -216,6 +262,10 @@ 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/java/io.mlw
+share/why3/stdlib/mach/java/lang.mlw
+share/why3/stdlib/mach/java/util.mlw
+share/why3/stdlib/mach/list.mlw
 share/why3/stdlib/mach/matrix.mlw
 share/why3/stdlib/mach/onetime.mlw
 share/why3/stdlib/mach/peano.mlw
@@ -223,7 +273,6 @@ 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
@@ -242,6 +291,7 @@ share/why3/stdlib/stack.mlw
 share/why3/stdlib/string.mlw
 share/why3/stdlib/tptp.mlw
 share/why3/stdlib/tree.mlw
+share/why3/stdlib/ufloat.mlw
 share/why3/stdlib/witness.mlw
 share/why3/vim/ftdetect/why3.vim
 share/why3/vim/syntax/why3.vim

Index: pkgsrc/devel/why3/distinfo
diff -u pkgsrc/devel/why3/distinfo:1.1 pkgsrc/devel/why3/distinfo:1.2
--- pkgsrc/devel/why3/distinfo:1.1      Sat Oct  8 16:36:47 2022
+++ pkgsrc/devel/why3/distinfo  Mon Mar  3 03:27:04 2025
@@ -1,5 +1,5 @@
-$NetBSD: distinfo,v 1.1 2022/10/08 16:36:47 tonio Exp $
+$NetBSD: distinfo,v 1.2 2025/03/03 03:27:04 dholland 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
+BLAKE2s (why3-1.8.0.tar.gz) = 34704a96ace3b7d6b795259ef6e06c03d6944d740af1c3b1f5567c108788863a
+SHA512 (why3-1.8.0.tar.gz) = 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549
+Size (why3-1.8.0.tar.gz) = 7373730 bytes

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

Home | Main Index | Thread Index | Old Index