this repo has no description

[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)

Changed files
+227
packages
dolmen
dolmen.0.9
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
+46
packages/dolmen/dolmen.0.9/opam
···
···
+
opam-version: "2.0"
+
maintainer: "Guillaume Bury <guillaume.bury@gmail.com>"
+
authors: "Guillaume Bury <guillaume.bury@gmail.com>"
+
license: "BSD-2-Clause"
+
build: [
+
["dune" "subst"] {dev}
+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
+
]
+
depends: [
+
"ocaml" {>= "4.08"}
+
"menhir" {>= "20211230" }
+
"dune" { >= "3.0" }
+
"fmt" { >= "0.8.7" }
+
"seq"
+
"odoc" { with-doc }
+
"qcheck" { with-test }
+
"mdx" { with-test }
+
]
+
+
tags: [ "parser" "logic" "tptp" "smtlib" "dimacs" ]
+
homepage: "https://github.com/Gbury/dolmen"
+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
+
bug-reports: "https://github.com/Gbury/dolmen/issues"
+
+
doc: "https://gbury.github.io/dolmen"
+
synopsis: "A parser library for automated deduction"
+
description:
+
"Dolmen is a parser library. It currently targets languages used in automated theorem provers,
+
but may be extended to other domains.
+
+
Dolmen provides functors that takes as arguments a representation of terms and statements,
+
and returns a module that can parse files (or streams of tokens) into the provided representation
+
of terms or statements. This is meant so that Dolmen can be used as a drop-in replacement of existing
+
parser, in order to factorize parsers among projects.
+
+
Additionally, Dolmen also provides a standard implementation of terms and statements that cna be
+
used ot instantiate its parsers."
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
+
checksum: [
+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
+
]
+
}
+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"
+42
packages/dolmen_bin/dolmen_bin.0.9/opam
···
···
+
opam-version: "2.0"
+
maintainer: "Guillaume Bury <guillaume.bury@gmail.com>"
+
authors: "Guillaume Bury <guillaume.bury@gmail.com>"
+
license: "BSD-2-Clause"
+
build: [
+
["dune" "subst"] {dev}
+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
+
]
+
depends: [
+
"ocaml" {>= "4.02.3"}
+
"dolmen" {= version }
+
"dolmen_type" {= version }
+
"dolmen_loop" {= version }
+
"dolmen_model" {= version }
+
"dune" { >= "3.0" }
+
"fmt"
+
"cmdliner" { >= "1.1.0" }
+
"odoc" { with-doc }
+
]
+
depopts: [
+
"memtrace"
+
]
+
tags: [ "logic" "computation" "automated theorem prover" "logic" "smtlib" "tptp"]
+
homepage: "https://github.com/Gbury/dolmen"
+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
+
bug-reports: "https://github.com/Gbury/dolmen/issues"
+
+
doc: "https://gbury.github.io/dolmen"
+
synopsis: "A linter for logic languages"
+
description:
+
"The dolmen binary is an instantiation of the Dolmen library
+
to provide a binary to easily parse and type files used in
+
automated deduction. "
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
+
checksum: [
+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
+
]
+
}
+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"
+37
packages/dolmen_loop/dolmen_loop.0.9/opam
···
···
+
opam-version: "2.0"
+
maintainer: "Guillaume Bury <guillaume.bury@gmail.com>"
+
authors: "Guillaume Bury <guillaume.bury@gmail.com>"
+
license: "BSD-2-Clause"
+
build: [
+
["dune" "subst"] {dev}
+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
+
]
+
depends: [
+
"ocaml" {>= "4.02.3"}
+
"dolmen" {= version }
+
"dolmen_type" {= version }
+
"dune" { >= "3.0" }
+
"gen"
+
"odoc" { with-doc }
+
"pp_loc" { >= "2.0.0" }
+
]
+
tags: [ "logic" "computation" "automated theorem prover" ]
+
homepage: "https://github.com/Gbury/dolmen"
+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
+
bug-reports: "https://github.com/Gbury/dolmen/issues"
+
+
doc: "https://gbury.github.io/dolmen"
+
synopsis: "A tool library for automated deduction tools"
+
description:
+
"Dolmen Loop is a library of useful helpers to parse
+
and loop over statements found in automated deduction files."
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
+
checksum: [
+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
+
]
+
}
+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"
+
+37
packages/dolmen_lsp/dolmen_lsp.0.9/opam
···
···
+
opam-version: "2.0"
+
maintainer: "Guillaume Bury <guillaume.bury@gmail.com>"
+
authors: "Guillaume Bury <guillaume.bury@gmail.com>"
+
license: "BSD-2-Clause"
+
build: [
+
["dune" "subst"] {dev}
+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
+
]
+
depends: [
+
"ocaml" {>= "4.02.3"}
+
"dolmen" {= version }
+
"dolmen_type" {= version }
+
"dolmen_loop" { = version }
+
"dune" { >= "3.0" }
+
"ocaml-syntax-shims"
+
"odoc" { with-doc }
+
"logs"
+
"lsp"
+
"linol" { >= "0.4" & < "0.5" }
+
"linol-lwt" { >= "0.4" & < "0.5" }
+
]
+
tags: [ "logic" "computation" "automated theorem prover" "lsp" "language server protocol"]
+
homepage: "https://github.com/Gbury/dolmen"
+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
+
bug-reports: "https://github.com/Gbury/dolmen/issues"
+
+
doc: "https://gbury.github.io/dolmen"
+
synopsis: "A LSP server for automated deduction languages"
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
+
checksum: [
+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
+
]
+
}
+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"
+33
packages/dolmen_model/dolmen_model.0.9/opam
···
···
+
opam-version: "2.0"
+
maintainer: "Guillaume Bury <guillaume.bury@gmail.com>"
+
authors: "Guillaume Bury <guillaume.bury@gmail.com>"
+
license: "BSD-2-Clause"
+
build: [
+
["dune" "subst"] {dev}
+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
+
]
+
depends: [
+
"ocaml" {>= "4.02.3"}
+
"dolmen" {= version }
+
"dolmen_loop" {= version }
+
"dune" { >= "3.0" }
+
"odoc" { with-doc }
+
"zarith" { >= "1.10" }
+
"farith"
+
]
+
tags: [ "logic" "type" "model" "modelchecking" "first order" ]
+
homepage: "https://github.com/Gbury/dolmen"
+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
+
bug-reports: "https://github.com/Gbury/dolmen/issues"
+
+
doc: "https://gbury.github.io/dolmen"
+
synopsis: "A model checker for automated deduction languages"
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
+
checksum: [
+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
+
]
+
}
+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"
+32
packages/dolmen_type/dolmen_type.0.9/opam
···
···
+
opam-version: "2.0"
+
maintainer: "Guillaume Bury <guillaume.bury@gmail.com>"
+
authors: "Guillaume Bury <guillaume.bury@gmail.com>"
+
license: "BSD-2-Clause"
+
build: [
+
["dune" "subst"] {dev}
+
["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc}]
+
]
+
depends: [
+
"ocaml" {>= "4.02.3"}
+
"dolmen" {= version }
+
"dune" { >= "3.0" }
+
"spelll" { >= "0.4" }
+
"uutf"
+
"odoc" { with-doc }
+
]
+
tags: [ "logic" "type" "typechecking" "first order" "polymorphism" ]
+
homepage: "https://github.com/Gbury/dolmen"
+
dev-repo: "git+https://github.com/Gbury/dolmen.git"
+
bug-reports: "https://github.com/Gbury/dolmen/issues"
+
+
doc: "https://gbury.github.io/dolmen"
+
synopsis: "A typechecker for automated deduction languages"
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.9/dolmen-0.9.tbz"
+
checksum: [
+
"sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a"
+
"sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74"
+
]
+
}
+
x-commit-hash: "d9f5abbaffe6e5daa4b06758db66134fe85c8c6a"