Log message:
why3: Disable emacs; otherwise it finds it and installs a .elc file

PKGREVISION -> 1

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

Log message:
Add missing dependency ocamlgraph

Log message:
Add missing dependency: coq

Log message:
why3: add missing ocaml-num dependency

still fails with PLIST issues

Log message:
Update devel/why3 to 1.5.1nb1

Make sure to install the library properly
This is necessary for frama-c to bind properly

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.