Ubuntu
why package

why 2.34-4ubuntu3 source package in Ubuntu

Changelog

why (2.34-4ubuntu3) xenial; urgency=medium

  * Drop build dependency on libfloat-coq, not buildable with the
    the current coq.
  * why still fails to build, so drop the the libwhy-coq binary
    and coq build dependency.

 -- Matthias Klose <email address hidden>  Tue, 23 Feb 2016 15:36:48 +0100

Upload details

Uploaded by:
Matthias Klose
Uploaded to:
Xenial
Original maintainer:
Debian OCaml Maintainers
Architectures:
any all
Section:
math
Urgency:
Medium Urgency

See full publishing history Publishing

Series Pocket Published Component Section

Downloads

File Size SHA-256 Checksum
why_2.34.orig.tar.gz 3.6 MiB 76f3af8cf3857424852ca76eb87c99ff6089aadc3271da6b829ca84529f9c733
why_2.34-4ubuntu3.debian.tar.xz 11.1 KiB 116b850889f67eb4944b4041d7e0b6c85982382080cc2b3f17a905ab07c4835c
why_2.34-4ubuntu3.dsc 2.2 KiB b8d7d82f2e60b9c3b01e9b5511df50a377349d32d19e37d4e1a17ecbd3b94b70

Available diffs

View changes file

Binary packages built by this source

why: Software verification tool

 Why aims at being a verification conditions generator (VCG) back-end
 for other verification tools. It provides a powerful input language
 including higher-order functions, polymorphism, references, arrays and
 exceptions. It generates proof obligations for many systems: the proof
 assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
 decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.

why-dbgsym: debug symbols for package why

 Why aims at being a verification conditions generator (VCG) back-end
 for other verification tools. It provides a powerful input language
 including higher-order functions, polymorphism, references, arrays and
 exceptions. It generates proof obligations for many systems: the proof
 assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
 decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.

why-examples: Examples of programs certified with Why

 Why aims at being a verification conditions generator (VCG) back-end
 for other verification tools. It provides a powerful input language
 including higher-order functions, polymorphism, references, arrays and
 exceptions. It generates proof obligations for many systems: the proof
 assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
 decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
 .
 This package contains examples of programs verified using Why.