Skip to content

Commit 3fcd6f5

Browse files
bobotbobot
committed
[new release] colibrilib, colibrics and colibri2 (0.4)
CHANGES: * Decision: Fix delayed decisions handling * Array: experimental theory * Quantifier: Improve eager instanciation heuristic * Quantifier: Avoid creating new term * Simplex: Fix redundant run * Fix compilation in 32bit * Fix sign of sqrt
1 parent ec44728 commit 3fcd6f5

File tree

3 files changed

+151
-0
lines changed
  • packages
    • colibri2/colibri2.0.4
    • colibrics/colibrics.0.4
    • colibrilib/colibrilib.0.4

3 files changed

+151
-0
lines changed

‎packages/colibri2/colibri2.0.4/opam‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
opam-version: "2.0"
2+
synopsis: "A CP solver for smtlib"
3+
description: "A reimplementation of COLIBRI in OCaml"
4+
maintainer: ["François Bobot"]
5+
authors: [
6+
"François Bobot"
7+
"Bruno Marre"
8+
"Guillaume Bury"
9+
"Stéphane Graham-Lengrand"
10+
]
11+
license: "LGPL-2.1-only"
12+
homepage: "https://colibri.frama-c.com"
13+
bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
14+
depends: [
15+
"colibrilib" {= version}
16+
"containers" {>= "3.6.1"}
17+
"dolmen" {>= "0.8"}
18+
"dolmen_type" {>= "0.8"}
19+
"dolmen_loop" {>= "0.8"}
20+
"cmdliner" {>= "1.1.1"}
21+
"base" {>= "v0.14.2"}
22+
"gen" {>= "1.0"}
23+
"re" {>= "1.10.3"}
24+
"ppx_here" {>= "v0.14.0"}
25+
"dune" {>= "3.0"}
26+
"dune-build-info"
27+
"zarith" {>= "1.12"}
28+
"ppx_deriving" {>= "5.2.1"}
29+
"ppx_optcomp" {>= "v0.14.3"}
30+
"ppx_hash" {>= "v0.14.0"}
31+
"ppx_inline_test" {>= "v0.14.1"}
32+
"ocamlgraph" {>= "2.0.0"}
33+
"qcheck-core" {>= "0.18.1"}
34+
"calcium"
35+
"farith"
36+
"ounit2" {>= "2.2.4" & with-test}
37+
"ocaml" {>= "4.12"}
38+
"ocplib-simplex" {= "0.4"}
39+
"odoc" {with-doc}
40+
]
41+
build: [
42+
["dune" "subst"] {dev}
43+
[
44+
"dune"
45+
"build"
46+
"-p"
47+
name
48+
"-j"
49+
jobs
50+
"@install"
51+
"@runtest" {with-test}
52+
"@doc" {with-doc}
53+
]
54+
]
55+
dev-repo: "git+https://git.frama-c.com/pub/colibrics.git"
56+
url {
57+
src:
58+
"https://git.frama-c.com/api/v4/projects/879/packages/generic/colibri2/0.4/colibri2-0.4.tbz"
59+
checksum: [
60+
"sha256=fe298191f4ae6af7046c6dee617da0100eba1738b11f868290d905cd0055ae27"
61+
"sha512=75aa7969bdbca6bef396e35d9660381c06ef21332730ecfb0a4dcc72596ef8575d5905ddd5341e0287e8e18a20db8df9d9894b698f98e11dfc6d26a183fc16f7"
62+
]
63+
}
64+
x-commit-hash: "a70aa3785c7a15d212b98885d4a0a494d141606c"

‎packages/colibrics/colibrics.0.4/opam‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
opam-version: "2.0"
2+
synopsis: "A CP solver proved in Why3"
3+
description: "The core of Colibrics is formally proved using Why3."
4+
maintainer: ["François Bobot"]
5+
authors: ["François Bobot"]
6+
license: "LGPL-2.1-only"
7+
homepage: "https://colibri.frama-c.com"
8+
bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
9+
depends: [
10+
"ppx_deriving_yojson" {>= "3.6.1"}
11+
"dolmen" {>= "0.8"}
12+
"dolmen_type" {>= "0.8"}
13+
"dolmen_loop" {>= "0.8"}
14+
"dune" {>= "3.0"}
15+
"zarith" {>= "1.12"}
16+
"cmdliner" {>= "1.1.1"}
17+
"ocaml" {>= "4.08"}
18+
"core" {>= "v0.14.1"}
19+
"jingoo" {>= "1.4.4"}
20+
"logs" {>= "0.7.0"}
21+
"why3" {>= "1.4.0"}
22+
"yojson"
23+
"ocaml" {>= "4.12"}
24+
"odoc" {with-doc}
25+
]
26+
build: [
27+
["dune" "subst"] {dev}
28+
[
29+
"dune"
30+
"build"
31+
"-p"
32+
name
33+
"-j"
34+
jobs
35+
"@install"
36+
"@runtest" {with-test}
37+
"@doc" {with-doc}
38+
]
39+
]
40+
dev-repo: "git+https://git.frama-c.com/pub/colibrics.git"
41+
url {
42+
src:
43+
"https://git.frama-c.com/api/v4/projects/879/packages/generic/colibri2/0.4/colibri2-0.4.tbz"
44+
checksum: [
45+
"sha256=fe298191f4ae6af7046c6dee617da0100eba1738b11f868290d905cd0055ae27"
46+
"sha512=75aa7969bdbca6bef396e35d9660381c06ef21332730ecfb0a4dcc72596ef8575d5905ddd5341e0287e8e18a20db8df9d9894b698f98e11dfc6d26a183fc16f7"
47+
]
48+
}
49+
x-commit-hash: "a70aa3785c7a15d212b98885d4a0a494d141606c"

‎packages/colibrilib/colibrilib.0.4/opam‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
opam-version: "2.0"
2+
synopsis: "A library of domains and propagators proved in Why3"
3+
description: "Interval, and union of interval domains defined formally"
4+
maintainer: ["François Bobot"]
5+
authors: ["François Bobot"]
6+
license: "LGPL-2.1-only"
7+
homepage: "https://colibri.frama-c.com"
8+
bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
9+
depends: [
10+
"dune" {>= "3.0"}
11+
"zarith" {>= "1.12"}
12+
"ocaml" {>= "4.12"}
13+
"odoc" {with-doc}
14+
]
15+
build: [
16+
["dune" "subst"] {dev}
17+
[
18+
"dune"
19+
"build"
20+
"-p"
21+
name
22+
"-j"
23+
jobs
24+
"@install"
25+
"@runtest" {with-test}
26+
"@doc" {with-doc}
27+
]
28+
]
29+
dev-repo: "git+https://git.frama-c.com/pub/colibrics.git"
30+
url {
31+
src:
32+
"https://git.frama-c.com/api/v4/projects/879/packages/generic/colibri2/0.4/colibri2-0.4.tbz"
33+
checksum: [
34+
"sha256=fe298191f4ae6af7046c6dee617da0100eba1738b11f868290d905cd0055ae27"
35+
"sha512=75aa7969bdbca6bef396e35d9660381c06ef21332730ecfb0a4dcc72596ef8575d5905ddd5341e0287e8e18a20db8df9d9894b698f98e11dfc6d26a183fc16f7"
36+
]
37+
}
38+
x-commit-hash: "a70aa3785c7a15d212b98885d4a0a494d141606c"

0 commit comments

Comments
 (0)