this repo has no description

[new release] dolmen (6 packages) (0.10)

CHANGES:

### UI

- Improved the printing of some data-structures (PR#190)

### Std

- Replace the `Plain` statement with the `Other` statement,
which is a more general version (PR#190)

### Parsing

- Treat quoted symbols from the stdlib as symbols, regardless of
their contents. Previously a `|assert|` would be understood as the
reserved work `assert`, allowing e.g. `(|assert| false)`. From now on
these are understood as symbols, so one can `(declare |assert| () Bool)`
(PR#198)
- Add parsing extensions for the smtlib2 language (PR#190, PR#194)
- Better split elements of clauses in `cnf` TPTP statements (PR#190)
- Ensure illegal chars raise the correct error during lexing
(Issue#191, PR#192)

### Printing

- Add printers for smtlib identifiers (PR#198)
- Printing of typed expressions (i.e. the Std.Expr module)
can now print the tags (PR#210)

### Typing

- Enforce some missing constraints on bitvectors
indexes and sizes for the smtlib2 BV theory (PR#172, PR#175)
- Slightly improve wording for errors and warnings concerning
non linearity and other arithmetic restrictions (PR#184)
- More information for reserved Id, resulting in more precise
errors when smt2 scripts use reserved ids (PR#193)
- Expose implicit declarations/definitions that happen during
typechecking (PR#199)
- Treat smtlib `:named` annotations as implicit definitions as
required by the spec (PR#199)
- Add a warning for unknown attributes in smtlib2. This replaces
the `unbound id` error that some files could raise before when
using non-standard attribtues (PR#207)
- Only type annotations on quantified formulas and binders once.
Previously, these were typed twice so that they can be attached to
both the body of the bound formula and the quantified formula itself.
(PR#207, PR#210)

### Loop

- Add the String theory to the ALL logic of smtlib2 (PR#182)

Changed files
+235
packages
dolmen
dolmen.0.10
dolmen_bin
dolmen_bin.0.10
dolmen_loop
dolmen_loop.0.10
dolmen_lsp
dolmen_lsp.0.10
dolmen_model
dolmen_model.0.10
dolmen_type
dolmen_type.0.10
+51
packages/dolmen/dolmen.0.10/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" }
+
"hmap" { >= "0.8.1" }
+
"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 aims at providing tools to help in writing programs in the field of theorem proving,
+
SMT solving, and model checking. The project includes a few libraries, a CLI binary and an
+
LSP server, split over several opam packages.
+
+
This is the Dolmen parser library. It currently targets languages used in automated theorem provers,
+
as well as model checking, and may be extended to other domains later.
+
+
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 can be
+
used to instantiate its parsers."
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.10/dolmen-0.10.tbz"
+
checksum: [
+
"sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
+
"sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f"
+
]
+
}
+
x-commit-hash: "c33632daab31fb3bb719031169baa6c984bb860f"
+42
packages/dolmen_bin/dolmen_bin.0.10/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, as well as verify models from theorem solvers."
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.10/dolmen-0.10.tbz"
+
checksum: [
+
"sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
+
"sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f"
+
]
+
}
+
x-commit-hash: "c33632daab31fb3bb719031169baa6c984bb860f"
+38
packages/dolmen_loop/dolmen_loop.0.10/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"
+
"pp_loc" { >= "2.0.0" }
+
"odoc" { with-doc }
+
"mdx" { with-test }
+
]
+
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.10/dolmen-0.10.tbz"
+
checksum: [
+
"sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
+
"sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f"
+
]
+
}
+
x-commit-hash: "c33632daab31fb3bb719031169baa6c984bb860f"
+
+37
packages/dolmen_lsp/dolmen_lsp.0.10/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.10/dolmen-0.10.tbz"
+
checksum: [
+
"sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
+
"sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f"
+
]
+
}
+
x-commit-hash: "c33632daab31fb3bb719031169baa6c984bb860f"
+35
packages/dolmen_model/dolmen_model.0.10/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:
+
"The Dolmen library for verifying models generated by
+
automated theorem provers and SMT solvers"
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.10/dolmen-0.10.tbz"
+
checksum: [
+
"sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
+
"sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f"
+
]
+
}
+
x-commit-hash: "c33632daab31fb3bb719031169baa6c984bb860f"
+32
packages/dolmen_type/dolmen_type.0.10/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: "The Dolmen library for typechecking languages"
+
url {
+
src:
+
"https://github.com/Gbury/dolmen/releases/download/v0.10/dolmen-0.10.tbz"
+
checksum: [
+
"sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
+
"sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f"
+
]
+
}
+
x-commit-hash: "c33632daab31fb3bb719031169baa6c984bb860f"