File: control

package info (click to toggle)
why 2.40-4
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 10,504 kB
  • sloc: ml: 71,410; xml: 13,660; java: 8,079; ansic: 1,176; makefile: 728; sh: 199; lisp: 3
file content (52 lines) | stat: -rw-r--r-- 1,629 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
Source: why
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Samuel Mimram <smimram@debian.org>,
  Mehdi Dogguy <mehdi@debian.org>,
  Ralf Treinen <treinen@debian.org>
Build-Depends:
  debhelper (>= 11),
  dh-ocaml (>= 0.9~),
  ocaml-nox (>= 4.02),
  camlp4,
  coq (>= 8.3~),
  libocamlgraph-ocaml-dev (>= 1.4~),
  libzarith-ocaml-dev,
  frama-c-base (>= 20171101+sulfur),
  camlidl,
  why3, why3-coq
Standards-Version: 4.1.4
Homepage: http://krakatoa.lri.fr/
Vcs-Browser: https://salsa.debian.org/ocaml-team/why
Vcs-Git: https://salsa.debian.org/ocaml-team/why.git

Package: why
Architecture: amd64 arm64 armhf hurd-i386 i386 kfreebsd-i386 kfreebsd-amd64 powerpc ppc64 ppc64el sparc s390x
Depends:
  ${shlibs:Depends},
  ${ocaml:Depends},
  ${misc:Depends},
  frama-c-base (= ${F:FramaCVersion}),
  why3,
  make
Suggests: libwhy-coq (= ${binary:Version})
Description: Software verification tool for C and Java
 This package contains Krakatoa and Jessie, two front-ends of the Why3
 platform for deductive program verification. Krakatoa deals with Java
 programs annotated in a variant of the The Java Modeling
 Language. Jessie deals with C programs annotated in the ANSI/ISO C
 Specification Language (ACSL).
 
Package: libwhy-coq
Architecture: all
Depends:
  ${misc:Depends},
  coq-${F:CoqABI}
Replaces:
  why (<< 2.18.dfsg-1)
Section: libdevel
Description: Why library for Coq
 This package contains all useful logical definitions, lemmas with their
 proofs and axioms used by Why. Users may need this package when proving
 some proof obligations in Coq.