Skip to content

Commit d886f1d

Browse files
bclement-ocpbclement-ocp
committed
[new release] alt-ergo (4 packages) (2.6.1)
CHANGES: - Consistent output of steps limit error (OCamlPro/alt-ergo#1245) - Prevent potential long-running loop without steps increase (OCamlPro/alt-ergo#1316) - Report correct number of steps when limit is exceeded (OCamlPro/alt-ergo#1317)
1 parent e6dedb1 commit d886f1d

File tree

4 files changed

+232
-0
lines changed
  • packages
    • alt-ergo-lib/alt-ergo-lib.2.6.1
    • alt-ergo-parsers/alt-ergo-parsers.2.6.1
    • alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.1
    • alt-ergo/alt-ergo.2.6.1

4 files changed

+232
-0
lines changed

‎packages/alt-ergo-lib/alt-ergo-lib.2.6.1/opam‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
opam-version: "2.0"
2+
synopsis: "The Alt-Ergo SMT prover library"
3+
description: """
4+
This is the core library used in the Alt-Ergo SMT solver.
5+
6+
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
7+
8+
See more details on http://alt-ergo.ocamlpro.com/"""
9+
maintainer: ["Alt-Ergo developers <[email protected]>"]
10+
authors: ["Alt-Ergo developers <[email protected]>"]
11+
homepage: "https://alt-ergo.ocamlpro.com/"
12+
doc: "https://ocamlpro.github.io/alt-ergo"
13+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
14+
depends: [
15+
"ocaml" {>= "4.08.1"}
16+
"dune" {>= "3.14"}
17+
"dune-build-info"
18+
"dolmen" {>= "0.10"}
19+
"dolmen_type" {>= "0.10"}
20+
"dolmen_loop" {>= "0.10"}
21+
"ocplib-simplex" {>= "0.5.1"}
22+
"zarith" {>= "1.11"}
23+
"seq"
24+
"fmt" {>= "0.9.0"}
25+
"stdlib-shims"
26+
"ppx_blob" {>= "0.7.2"}
27+
"ppx_deriving"
28+
"camlzip" {>= "1.07"}
29+
"odoc" {with-doc}
30+
"ppx_deriving"
31+
"qcheck" {with-test & = "0.22"}
32+
]
33+
conflicts: [
34+
"ppxlib" {< "0.30.0"}
35+
"result" {< "1.5"}
36+
]
37+
build: [
38+
["dune" "subst"] {dev}
39+
[
40+
"dune"
41+
"build"
42+
"-p"
43+
name
44+
"-j"
45+
jobs
46+
"--promote-install-files=false"
47+
"@install"
48+
"@runtest" {with-test}
49+
"@doc" {with-doc}
50+
]
51+
["dune" "install" "-p" name "--create-install-files" name]
52+
]
53+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
54+
# This part comes from the template. Please edit alt-ergo-lib.opam.template
55+
# and not alt-ergo-lib.opam which is generated by dune
56+
tags: "org:OCamlPro"
57+
58+
license: [
59+
"LicenseRef-OCamlpro-Non-Commercial"
60+
"Apache-2.0"
61+
]
62+
url {
63+
src:
64+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.1/alt-ergo-2.6.1.tbz"
65+
checksum: [
66+
"sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba"
67+
"sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb"
68+
]
69+
}
70+
x-commit-hash: "80cf48b3b878b416dea7500a060132c024bf69c4"

‎packages/alt-ergo-parsers/alt-ergo-parsers.2.6.1/opam‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
opam-version: "2.0"
2+
synopsis: "The Alt-Ergo SMT prover parser library"
3+
description: """
4+
This is the parser library used in the Alt-Ergo SMT solver.
5+
6+
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
7+
8+
See more details on http://alt-ergo.ocamlpro.com/"""
9+
maintainer: ["Alt-Ergo developers <[email protected]>"]
10+
authors: ["Alt-Ergo developers <[email protected]>"]
11+
homepage: "https://alt-ergo.ocamlpro.com/"
12+
doc: "https://ocamlpro.github.io/alt-ergo"
13+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
14+
depends: [
15+
"ocaml" {>= "4.08.1"}
16+
"dune" {>= "3.14"}
17+
"alt-ergo-lib" {= version}
18+
"psmt2-frontend" {>= "0.4"}
19+
"menhir"
20+
"stdlib-shims"
21+
"odoc" {with-doc}
22+
]
23+
build: [
24+
["dune" "subst"] {dev}
25+
[
26+
"dune"
27+
"build"
28+
"-p"
29+
name
30+
"-j"
31+
jobs
32+
"--promote-install-files=false"
33+
"@install"
34+
"@runtest" {with-test}
35+
"@doc" {with-doc}
36+
]
37+
["dune" "install" "-p" name "--create-install-files" name]
38+
]
39+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
40+
# This part comes from the template. Please edit alt-ergo-parsers.opam.template
41+
# and not alt-ergo-parsers.opam which is generated by dune
42+
tags: "org:OCamlPro"
43+
44+
license: [
45+
"LicenseRef-OCamlpro-Non-Commercial"
46+
"Apache-2.0"
47+
]
48+
url {
49+
src:
50+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.1/alt-ergo-2.6.1.tbz"
51+
checksum: [
52+
"sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba"
53+
"sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb"
54+
]
55+
}
56+
x-commit-hash: "80cf48b3b878b416dea7500a060132c024bf69c4"

‎packages/alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.1/opam‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
opam-version: "2.0"
2+
synopsis: "An experimental Why3 frontend for Alt-Ergo"
3+
description: """
4+
An experimental front-end that parses a subset of Why3's logic. More
5+
precisely, this front-end targets proof obligations generated by the
6+
Atelier-B framework in Why3 format. It should be used with a prelude
7+
defining the B Set theory."""
8+
maintainer: ["Alt-Ergo developers <[email protected]>"]
9+
authors: ["Alt-Ergo developers <[email protected]>"]
10+
license: "LGPL-2.1-only"
11+
homepage: "https://alt-ergo.ocamlpro.com/"
12+
doc: "https://ocamlpro.github.io/alt-ergo"
13+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
14+
depends: [
15+
"dune" {>= "3.14"}
16+
"alt-ergo" {= version}
17+
"alt-ergo-lib" {= version}
18+
"alt-ergo-parsers" {= version}
19+
"odoc" {with-doc}
20+
]
21+
build: [
22+
["dune" "subst"] {dev}
23+
[
24+
"dune"
25+
"build"
26+
"-p"
27+
name
28+
"-j"
29+
jobs
30+
"--promote-install-files=false"
31+
"@install"
32+
"@runtest" {with-test}
33+
"@doc" {with-doc}
34+
]
35+
["dune" "install" "-p" name "--create-install-files" name]
36+
]
37+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
38+
# This part comes from the template. Please edit
39+
# alt-ergo-plugin-ab-why3.opam.template and not alt-ergo-plugin-ab-why3.opam
40+
# which is generated by dune
41+
42+
conflicts: [ "ocaml-option-bytecode-only" ]
43+
url {
44+
src:
45+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.1/alt-ergo-2.6.1.tbz"
46+
checksum: [
47+
"sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba"
48+
"sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb"
49+
]
50+
}
51+
x-commit-hash: "80cf48b3b878b416dea7500a060132c024bf69c4"

‎packages/alt-ergo/alt-ergo.2.6.1/opam‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
opam-version: "2.0"
2+
synopsis: "The Alt-Ergo SMT prover"
3+
description: """
4+
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
5+
6+
See more details on https://alt-ergo.ocamlpro.com/"""
7+
maintainer: ["Alt-Ergo developers <[email protected]>"]
8+
authors: ["Alt-Ergo developers <[email protected]>"]
9+
homepage: "https://alt-ergo.ocamlpro.com/"
10+
doc: "https://ocamlpro.github.io/alt-ergo"
11+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
12+
depends: [
13+
"ocaml" {>= "4.08.1"}
14+
"dune" {>= "3.14"}
15+
"alt-ergo-lib" {= version}
16+
"alt-ergo-parsers" {= version}
17+
"menhir"
18+
"dune-site"
19+
"cmdliner" {>= "1.1.0" & < "2.0"}
20+
"odoc" {with-doc}
21+
]
22+
build: [
23+
["dune" "subst"] {dev}
24+
[
25+
"dune"
26+
"build"
27+
"-p"
28+
name
29+
"-j"
30+
jobs
31+
"--promote-install-files=false"
32+
"@install"
33+
"@runtest" {with-test}
34+
"@doc" {with-doc}
35+
]
36+
["dune" "install" "-p" name "--create-install-files" name]
37+
]
38+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
39+
# This part comes from the template. Please edit alt-ergo.opam.template
40+
# and not alt-ergo.opam which is generated by dune
41+
tags: "org:OCamlPro"
42+
43+
license: [
44+
"LicenseRef-OCamlpro-Non-Commercial"
45+
"Apache-2.0"
46+
]
47+
url {
48+
src:
49+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.1/alt-ergo-2.6.1.tbz"
50+
checksum: [
51+
"sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba"
52+
"sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb"
53+
]
54+
}
55+
x-commit-hash: "80cf48b3b878b416dea7500a060132c024bf69c4"

0 commit comments

Comments
 (0)