this repo has no description
Why3 1.8.0
+222
+67
packages/why3-coq/why3-coq.1.8.0/opam
+67
packages/why3-coq/why3-coq.1.8.0/opam
···
1
+
opam-version: "2.0"
2
+
maintainer: "guillaume.melquiond@inria.fr"
3
+
authors: [
4
+
"François Bobot"
5
+
"Jean-Christophe Filliâtre"
6
+
"Claude Marché"
7
+
"Guillaume Melquiond"
8
+
"Andrei Paskevich"
9
+
]
10
+
11
+
homepage: "https://www.why3.org/"
12
+
license: "LGPL-2.1-only"
13
+
doc: "https://www.why3.org/doc/"
14
+
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
15
+
dev-repo: "git+https://gitlab.inria.fr/why3/why3.git"
16
+
17
+
tags: [
18
+
"deductive"
19
+
"program verification"
20
+
"formal specification"
21
+
"automated theorem prover"
22
+
"interactive theorem prover"
23
+
]
24
+
25
+
build: [
26
+
["./autogen.sh"] {dev} # when pinning, there might be no configure file
27
+
["touch" "configure"]
28
+
["./configure"
29
+
"--prefix" prefix
30
+
"--disable-why3-lib"
31
+
"--disable-frama-c"
32
+
"--disable-ide"
33
+
"--disable-js-of-ocaml"
34
+
"--enable-coq-libs"]
35
+
[make "-j%{jobs}%" "coq"]
36
+
]
37
+
38
+
install: [make "install-coq"]
39
+
40
+
depends: [
41
+
"conf-autoconf" {build & dev}
42
+
"coq" {>= "8.16"}
43
+
"ocaml" {>= "4.08.0"}
44
+
"ocamlfind" {build}
45
+
"why3" {= version}
46
+
]
47
+
48
+
depopts: [
49
+
"coq-flocq" {>= "3.4"}
50
+
]
51
+
52
+
synopsis: "Why3 environment for deductive program verification"
53
+
54
+
description: """
55
+
Why3 provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.
56
+
57
+
Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
58
+
59
+
This package provides the Coq realizations of Why3 theories."""
60
+
61
+
url {
62
+
src: "https://why3.gitlabpages.inria.fr/releases/why3-1.8.0.tar.gz"
63
+
checksum: [
64
+
"sha256=8037b8388d00ba86262520a0fd23114187207a55ff48cdbc0a541f2a19f0f3c1"
65
+
"md5=06dd02f87aa1a698f90f1f5eaf234920"
66
+
]
67
+
}
+66
packages/why3-ide/why3-ide.1.8.0/opam
+66
packages/why3-ide/why3-ide.1.8.0/opam
···
1
+
opam-version: "2.0"
2
+
maintainer: "guillaume.melquiond@inria.fr"
3
+
authors: [
4
+
"François Bobot"
5
+
"Jean-Christophe Filliâtre"
6
+
"Claude Marché"
7
+
"Guillaume Melquiond"
8
+
"Andrei Paskevich"
9
+
]
10
+
11
+
homepage: "https://www.why3.org/"
12
+
license: "LGPL-2.1-only"
13
+
doc: "https://www.why3.org/doc/"
14
+
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
15
+
dev-repo: "git+https://gitlab.inria.fr/why3/why3.git"
16
+
17
+
tags: [
18
+
"deductive"
19
+
"program verification"
20
+
"formal specification"
21
+
"automated theorem prover"
22
+
"interactive theorem prover"
23
+
]
24
+
25
+
build: [
26
+
["./autogen.sh"] {dev} # when pinning, there might be no configure file
27
+
["touch" "configure"]
28
+
["./configure"
29
+
"--prefix" prefix
30
+
"--disable-why3-lib"
31
+
"--disable-frama-c"
32
+
"--disable-coq-libs"
33
+
"--disable-js-of-ocaml"
34
+
"--disable-re"
35
+
"--enable-ocamlfind"
36
+
"--enable-ide"]
37
+
[make "-j%{jobs}%" "ide"]
38
+
]
39
+
40
+
install: [make "install-ide"]
41
+
42
+
depends: [
43
+
"conf-autoconf" {build & dev}
44
+
"ocaml" {>= "4.08.0"}
45
+
"ocamlfind" {build}
46
+
"why3" {= version}
47
+
"lablgtk3"
48
+
"lablgtk3-sourceview3"
49
+
]
50
+
51
+
synopsis: "Why3 environment for deductive program verification"
52
+
53
+
description: """
54
+
Why3 provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.
55
+
56
+
Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
57
+
58
+
This package provides an IDE for Why3."""
59
+
60
+
url {
61
+
src: "https://why3.gitlabpages.inria.fr/releases/why3-1.8.0.tar.gz"
62
+
checksum: [
63
+
"sha256=8037b8388d00ba86262520a0fd23114187207a55ff48cdbc0a541f2a19f0f3c1"
64
+
"md5=06dd02f87aa1a698f90f1f5eaf234920"
65
+
]
66
+
}
+89
packages/why3/why3.1.8.0/opam
+89
packages/why3/why3.1.8.0/opam
···
1
+
opam-version: "2.0"
2
+
maintainer: "guillaume.melquiond@inria.fr"
3
+
authors: [
4
+
"François Bobot"
5
+
"Jean-Christophe Filliâtre"
6
+
"Claude Marché"
7
+
"Guillaume Melquiond"
8
+
"Andrei Paskevich"
9
+
]
10
+
11
+
homepage: "https://www.why3.org/"
12
+
license: "LGPL-2.1-only"
13
+
doc: "https://www.why3.org/doc/"
14
+
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
15
+
dev-repo: "git+https://gitlab.inria.fr/why3/why3.git"
16
+
17
+
tags: [
18
+
"deductive"
19
+
"program verification"
20
+
"formal specification"
21
+
"automated theorem prover"
22
+
"interactive theorem prover"
23
+
]
24
+
25
+
build: [
26
+
["./autogen.sh"] {dev} # when pinning, there might be no configure file
27
+
["touch" "configure"]
28
+
["./configure"
29
+
"--prefix" prefix
30
+
"--disable-frama-c"
31
+
"--disable-coq-libs"
32
+
"--disable-js-of-ocaml"
33
+
"--disable-re"
34
+
"--enable-ocamlfind"
35
+
"--disable-mpfr" {!mlmpfr:installed}
36
+
"--enable-mpfr" {mlmpfr:installed}
37
+
"--disable-zip" {!camlzip:installed}
38
+
"--enable-zip" {camlzip:installed}
39
+
"--disable-hypothesis-selection" {!ocamlgraph:installed}
40
+
"--enable-hypothesis-selection" {ocamlgraph:installed}
41
+
"--disable-stackify" {!ocamlgraph:installed}
42
+
"--enable-stackify" {ocamlgraph:installed}
43
+
"--disable-ide"]
44
+
[make "-j%{jobs}%" "all" "byte"]
45
+
[make "doc" "stdlibdoc" "apidoc"] {with-doc}
46
+
]
47
+
48
+
install: [
49
+
[make "install" "install-lib"]
50
+
[make "DOCDIR=%{_:doc}%" "install-doc"] {with-doc}
51
+
]
52
+
53
+
depends: [
54
+
"conf-autoconf" {build & dev}
55
+
"ocaml" {>= "4.09"}
56
+
"ocamlfind" {build}
57
+
"menhir" {>= "20200211"}
58
+
"zarith"
59
+
]
60
+
61
+
depopts: [
62
+
"camlzip"
63
+
"ocamlgraph"
64
+
"sexplib"
65
+
"ppx_deriving" {build}
66
+
"ppx_sexp_conv" {build}
67
+
"mlmpfr"
68
+
]
69
+
70
+
conflicts: [
71
+
"why3-base"
72
+
"ocamlgraph" {< "1.8.2"}
73
+
"mlmpfr" {< "4.0.0"}
74
+
]
75
+
76
+
synopsis: "Why3 environment for deductive program verification"
77
+
78
+
description: """
79
+
Why3 provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.
80
+
81
+
Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted."""
82
+
83
+
url {
84
+
src: "https://why3.gitlabpages.inria.fr/releases/why3-1.8.0.tar.gz"
85
+
checksum: [
86
+
"sha256=8037b8388d00ba86262520a0fd23114187207a55ff48cdbc0a541f2a19f0f3c1"
87
+
"md5=06dd02f87aa1a698f90f1f5eaf234920"
88
+
]
89
+
}