Skip to content

Commit a5d053e

Browse files
GburyGbury
committed
[new release] dolmen_type, dolmen_model, dolmen_lsp, dolmen_loop, dolmen_bin and dolmen (0.9)
CHANGES: ### Doc - Add examples in the doc and tuto for type-checking (including a minimal working example in the tutorial). ### UI - Make the unknown logic fatal by default, and simply enabled in non-strict mode (PR#158) - Add the `--check-flow` option to checks coherence of sequences of statements (PR#135) - Ensure stability of error codes for the `dolmen` binary ### Parsing - Add `attrs` fields for all declarations and definition types, and correctly attach predicate attribute to individual definitions (PR#130) - Restore support for toplevel "and" in non-recursive predicate/function definitions in Alt-Ergo syntax (PR Gbury/dolmen#147, fixes issue Gbury/dolmen#144) - Add support for hexadecimal floats in Alt-Ergo syntax (PR Gbury/dolmen#148, fixes issue Gbury/dolmen#145) - Add local goals to the `Prove` statement (PR#140) - Add a check-sat/prove-sat statement to ae's language (PR#140) ### Typing - Ignore arithmetic restrictions when typing model values. This particularly affects difference logic (PR#141) - Rename theory-specific configuration to `config` (instead of `arith`, `arrays`, etc..) (PR#142) - Add printing function for logics (PR#142) - Attach type definitions to type-defs (PR#157) - Add a proper reason for reserved builtins (PR#155) - Add bitvector builtins for alt-ergo's language (PR#136) ### Loop - Add possibility for users of the loop library to choose the exit/return code for a `Code.t` (PR#134) - Add the `Flow` module for flow checking (PR#135) - Add the `check` function in `typer.ml`/`typer_intf.ml` - Add `update` and `update_opt` in `State` (PR#156) - Print type definitions in the printer of typed statements (PR#157) - Prelude statements have been removed and replaced with prelude files (PR#160) - `Typer.additional_builtins` is now a `State.key` and takes the current state and language as arguments (PR#160) ### Model - Fix bug in bitvector implementation: negative inputs to `bvsmod` would raise an internal error (PR#138) - Remove the "error" keyword and statement from smtlib2 response (model) files (PR#139) - Correctly compare abstract array values (PR#143) - Accept extensions of functions/symbols with only partially defined semantics, for e.g. `fp.to_ubv`, `div`, etc.. (PR#151) - Error out on incremental problems (PR#169)
1 parent 3befa84 commit a5d053e

File tree

6 files changed

+227
-0
lines changed
  • packages
    • dolmen_bin/dolmen_bin.0.9
    • dolmen_loop/dolmen_loop.0.9
    • dolmen_lsp/dolmen_lsp.0.9
    • dolmen_model/dolmen_model.0.9
    • dolmen_type/dolmen_type.0.9
    • dolmen/dolmen.0.9

6 files changed

+227
-0
lines changed

‎packages/dolmen/dolmen.0.9/opam‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
opam-version: "2.0"
2+
maintainer: "Guillaume Bury <[email protected]>"
3+
authors: "Guillaume Bury <[email protected]>"
4+
license: "BSD-2-Clause"
5+
build: [
6+
["dune" "subst"] {dev}
7+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
8+
]
9+
depends: [
10+
"ocaml" {>= "4.08"}
11+
"menhir" {>= "20211230" }
12+
"dune" { >= "3.0" }
13+
"fmt" { >= "0.8.7" }
14+
"seq"
15+
"odoc" { with-doc }
16+
"qcheck" { with-test }
17+
"mdx" { with-test }
18+
]
19+
20+
tags: [ "parser" "logic" "tptp" "smtlib" "dimacs" ]
21+
homepage: "https://github.com/Gbury/dolmen"
22+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
23+
bug-reports: "https://github.com/Gbury/dolmen/issues"
24+
25+
doc: "https://gbury.github.io/dolmen"
26+
synopsis: "A parser library for automated deduction"
27+
description:
28+
"Dolmen is a parser library. It currently targets languages used in automated theorem provers,
29+
but may be extended to other domains.
30+
31+
Dolmen provides functors that takes as arguments a representation of terms and statements,
32+
and returns a module that can parse files (or streams of tokens) into the provided representation
33+
of terms or statements. This is meant so that Dolmen can be used as a drop-in replacement of existing
34+
parser, in order to factorize parsers among projects.
35+
36+
Additionally, Dolmen also provides a standard implementation of terms and statements that cna be
37+
used ot instantiate its parsers."
38+
url {
39+
src:
40+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
41+
checksum: [
42+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
43+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
44+
]
45+
}
46+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"

‎packages/dolmen_bin/dolmen_bin.0.9/opam‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
opam-version: "2.0"
2+
maintainer: "Guillaume Bury <[email protected]>"
3+
authors: "Guillaume Bury <[email protected]>"
4+
license: "BSD-2-Clause"
5+
build: [
6+
["dune" "subst"] {dev}
7+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
8+
]
9+
depends: [
10+
"ocaml" {>= "4.02.3"}
11+
"dolmen" {= version }
12+
"dolmen_type" {= version }
13+
"dolmen_loop" {= version }
14+
"dolmen_model" {= version }
15+
"dune" { >= "3.0" }
16+
"fmt"
17+
"cmdliner" { >= "1.1.0" }
18+
"odoc" { with-doc }
19+
]
20+
depopts: [
21+
"memtrace"
22+
]
23+
tags: [ "logic" "computation" "automated theorem prover" "logic" "smtlib" "tptp"]
24+
homepage: "https://github.com/Gbury/dolmen"
25+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
26+
bug-reports: "https://github.com/Gbury/dolmen/issues"
27+
28+
doc: "https://gbury.github.io/dolmen"
29+
synopsis: "A linter for logic languages"
30+
description:
31+
"The dolmen binary is an instantiation of the Dolmen library
32+
to provide a binary to easily parse and type files used in
33+
automated deduction. "
34+
url {
35+
src:
36+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
37+
checksum: [
38+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
39+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
40+
]
41+
}
42+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"

‎packages/dolmen_loop/dolmen_loop.0.9/opam‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
opam-version: "2.0"
2+
maintainer: "Guillaume Bury <[email protected]>"
3+
authors: "Guillaume Bury <[email protected]>"
4+
license: "BSD-2-Clause"
5+
build: [
6+
["dune" "subst"] {dev}
7+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
8+
]
9+
depends: [
10+
"ocaml" {>= "4.02.3"}
11+
"dolmen" {= version }
12+
"dolmen_type" {= version }
13+
"dune" { >= "3.0" }
14+
"gen"
15+
"odoc" { with-doc }
16+
"pp_loc" { >= "2.0.0" }
17+
]
18+
tags: [ "logic" "computation" "automated theorem prover" ]
19+
homepage: "https://github.com/Gbury/dolmen"
20+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
21+
bug-reports: "https://github.com/Gbury/dolmen/issues"
22+
23+
doc: "https://gbury.github.io/dolmen"
24+
synopsis: "A tool library for automated deduction tools"
25+
description:
26+
"Dolmen Loop is a library of useful helpers to parse
27+
and loop over statements found in automated deduction files."
28+
url {
29+
src:
30+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
31+
checksum: [
32+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
33+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
34+
]
35+
}
36+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"
37+

‎packages/dolmen_lsp/dolmen_lsp.0.9/opam‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
opam-version: "2.0"
2+
maintainer: "Guillaume Bury <[email protected]>"
3+
authors: "Guillaume Bury <[email protected]>"
4+
license: "BSD-2-Clause"
5+
build: [
6+
["dune" "subst"] {dev}
7+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
8+
]
9+
depends: [
10+
"ocaml" {>= "4.02.3"}
11+
"dolmen" {= version }
12+
"dolmen_type" {= version }
13+
"dolmen_loop" { = version }
14+
"dune" { >= "3.0" }
15+
"ocaml-syntax-shims"
16+
"odoc" { with-doc }
17+
"logs"
18+
"lsp"
19+
"linol" { >= "0.4" & < "0.5" }
20+
"linol-lwt" { >= "0.4" & < "0.5" }
21+
]
22+
tags: [ "logic" "computation" "automated theorem prover" "lsp" "language server protocol"]
23+
homepage: "https://github.com/Gbury/dolmen"
24+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
25+
bug-reports: "https://github.com/Gbury/dolmen/issues"
26+
27+
doc: "https://gbury.github.io/dolmen"
28+
synopsis: "A LSP server for automated deduction languages"
29+
url {
30+
src:
31+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
32+
checksum: [
33+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
34+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
35+
]
36+
}
37+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"

‎packages/dolmen_model/dolmen_model.0.9/opam‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
opam-version: "2.0"
2+
maintainer: "Guillaume Bury <[email protected]>"
3+
authors: "Guillaume Bury <[email protected]>"
4+
license: "BSD-2-Clause"
5+
build: [
6+
["dune" "subst"] {dev}
7+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
8+
]
9+
depends: [
10+
"ocaml" {>= "4.02.3"}
11+
"dolmen" {= version }
12+
"dolmen_loop" {= version }
13+
"dune" { >= "3.0" }
14+
"odoc" { with-doc }
15+
"zarith" { >= "1.10" }
16+
"farith"
17+
]
18+
tags: [ "logic" "type" "model" "modelchecking" "first order" ]
19+
homepage: "https://github.com/Gbury/dolmen"
20+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
21+
bug-reports: "https://github.com/Gbury/dolmen/issues"
22+
23+
doc: "https://gbury.github.io/dolmen"
24+
synopsis: "A model checker for automated deduction languages"
25+
url {
26+
src:
27+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
28+
checksum: [
29+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
30+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
31+
]
32+
}
33+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"

‎packages/dolmen_type/dolmen_type.0.9/opam‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
opam-version: "2.0"
2+
maintainer: "Guillaume Bury <[email protected]>"
3+
authors: "Guillaume Bury <[email protected]>"
4+
license: "BSD-2-Clause"
5+
build: [
6+
["dune" "subst"] {dev}
7+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
8+
]
9+
depends: [
10+
"ocaml" {>= "4.02.3"}
11+
"dolmen" {= version }
12+
"dune" { >= "3.0" }
13+
"spelll" { >= "0.4" }
14+
"uutf"
15+
"odoc" { with-doc }
16+
]
17+
tags: [ "logic" "type" "typechecking" "first order" "polymorphism" ]
18+
homepage: "https://github.com/Gbury/dolmen"
19+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
20+
bug-reports: "https://github.com/Gbury/dolmen/issues"
21+
22+
doc: "https://gbury.github.io/dolmen"
23+
synopsis: "A typechecker for automated deduction languages"
24+
url {
25+
src:
26+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
27+
checksum: [
28+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
29+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
30+
]
31+
}
32+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"

0 commit comments

Comments
 (0)