./math/gappa, Formal verification tool for numerical programs

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 1.6.1, Package name: gappa-1.6.1, Maintainer: pkgsrc-users

Gappa is a tool intended to help verifying and formally proving
properties on numerical programs dealing with floating-point or
fixed-point arithmetic.


Required to run:
[math/mpfr] [devel/gmp]

Required to build:
[devel/boost-headers] [pkgtools/cwrappers]

Master sites:

Filesize: 390.701 KB

Version history: (Expand)

CVS history: (Expand)


   2026-01-09 21:30:29 by Alexander Nasonov | Files touched by this commit (3) | Package updated
Log message:
Update math/gappa to version 1.6.1.

Version 1.6.1
-------------

D2 back-end
  * added support for D2 0.6.9; previous versions are no longer supported

Build system
  * fixed compilation with GCC 14

Version 1.6.0
-------------

Fact database
  * fixed `add_flt_lin` and `add_flt_lin_rev`
  * changed some rewriting rules about quotients into rules about `LIN`

Arithmetic
  * removed support for homogeneous and relative rounding functions

Version 1.5.0
-------------

Fact database
  * added predicate `LIN`: `x = y * e`
  * used `LIN(a, b)` for properties of the kind `BND(a / b)`
  * generalized Sterbenz-like theorems
  * specified `x / 0` as being equal to `0`, which removes some `NZR` hypotheses

Syntax
  * added binary operator `//` to denote `LIN` properties

Back-ends
  * added a back-end to produce D2 files

Coq script back-end
  * removed the use of `Notation` as it causes a huge slowdown in the prover

Version 1.4.2
-------------

Build system
  * regenerated using a recent version of Autoconf

Version 1.4.1
-------------

Coq back-end
  * registered a few more theorems

Whole engine
  * fixed crash on negative literals in rewriting rules

Version 1.4.0
-------------

Syntax
  * changed precedence of unary minus,
    e.g., `- 1` is parsed as `-(1)`, `-1*x` as `(-1)*x`,
    `- 1*x` as `-(1*x)`, `-x*1` as `-(x*1)`
  * allowed `;` as a separator for interval bounds, e.g., `[1;2]`
  * allowed `p` as exponent after a decimal integer, e.g., `1p2`

Proof paths
  * decreased amount of pointless lemmas

Documentation
  * moved to reST

Build system
  * added support for DESTDIR during installation

Licensing
  * updated CeCILL from 2.0 to 2.1 and GPL from 2 to 3
   2025-09-27 11:57:41 by Thomas Klausner | Files touched by this commit (337) 
Log message:
*: recursive bump for boost 1.89
   2023-09-01 12:17:26 by Nia Alarie | Files touched by this commit (1) 
Log message:
gappa: Assumes compiler defaults to C++11.
   2021-10-26 12:56:13 by Nia Alarie | Files touched by this commit (458) 
Log message:
math: Replace RMD160 checksums with BLAKE2s checksums

All checksums have been double-checked against existing RMD160 and
SHA512 hashes
   2021-10-07 16:28:36 by Nia Alarie | Files touched by this commit (458) 
Log message:
math: Remove SHA1 hashes for distfiles
   2020-07-17 19:30:14 by Taylor R Campbell | Files touched by this commit (6) 
Log message:
math/gappa, math/sollya: Cite upstreamed patches.
   2020-05-24 00:59:31 by Taylor R Campbell | Files touched by this commit (1) 
Log message:
Fix patchsum.
   2020-05-19 23:42:29 by Taylor R Campbell | Files touched by this commit (5) 
Log message:
gappa: Import gappa-1.3.5 as math-gappa

Gappa is a tool intended to help verifying and formally proving
properties on numerical programs dealing with floating-point or
fixed-point arithmetic.