this repo has no description

[new release] dolmen_type, dolmen_model, dolmen_lsp, dolmen_loop, dolmen_bin and dolmen (0.8.1)

CHANGES:

### UI

- Fix handling of size/time limits on windows (PR#117)
- Fix spurious printing of backtraces (PR#118)
- Add release binaries for windows

### LSP

- Add option for the lsp to read preludes before checking
each file (PR#116)
- The LSP now sends an empty list of diagnostics upon closing
a file (PR#116)

### Parsing

- Fix a bug related to alt-ergos function definition, which
were previously alwyas non-recursive. Now, alt-ergo's function
definitions are always recursive (PR#123)
- Add `parse_raw_lazy` to parse a string into a lazy list of
statements (PR#125)
- Add support for mutually recursive functions and predicates
in Alt-ergo's native language (PR#129)

### Typing

- Properly add binding locations for implicit type variables
(PR#123)
- Ensure that type of recursively defined symbols are freshened
to avoid type variables sharing between declaration and
definition (PR#123)

### Loop

- Use `GC.finalise` instead of `Gc.finalise_last` in `loop/parser.ml`
in order to avoid a bug in the ocaml 5.0 runtime, see ocaml/ocaml#12001
(PR#128)
- New module to implement Alarms (size/time limits) (PR#117)
- Add optional argument to `Pipeline.run` to specify
an alarm implementation (PR#117)
- Add a `bt` key to the state to record whether we should print
backtraces (PR#118)
- Use `parse_raw_lazy` to parse raw contents in full mode if/when
necessary (PR#125)

Changed files
+227
packages
dolmen
dolmen.0.8.1
dolmen_bin
dolmen_bin.0.8.1
dolmen_loop
dolmen_loop.0.8.1
dolmen_lsp
dolmen_lsp.0.8.1
dolmen_model
dolmen_model.0.8.1
dolmen_type
dolmen_type.0.8.1
+46
packages/dolmen/dolmen.0.8.1/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.8.1/dolmen-0.8.1.tbz"
+
checksum: [
+
"sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928"
+
"sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04"
+
]
+
}
+
x-commit-hash: "30acfc9d8751fdf88b9288943aaa3481fc7254a6"
+42
packages/dolmen_bin/dolmen_bin.0.8.1/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.8.1/dolmen-0.8.1.tbz"
+
checksum: [
+
"sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928"
+
"sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04"
+
]
+
}
+
x-commit-hash: "30acfc9d8751fdf88b9288943aaa3481fc7254a6"
+37
packages/dolmen_loop/dolmen_loop.0.8.1/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.8.1/dolmen-0.8.1.tbz"
+
checksum: [
+
"sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928"
+
"sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04"
+
]
+
}
+
x-commit-hash: "30acfc9d8751fdf88b9288943aaa3481fc7254a6"
+
+37
packages/dolmen_lsp/dolmen_lsp.0.8.1/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.8.1/dolmen-0.8.1.tbz"
+
checksum: [
+
"sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928"
+
"sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04"
+
]
+
}
+
x-commit-hash: "30acfc9d8751fdf88b9288943aaa3481fc7254a6"
+33
packages/dolmen_model/dolmen_model.0.8.1/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.8.1/dolmen-0.8.1.tbz"
+
checksum: [
+
"sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928"
+
"sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04"
+
]
+
}
+
x-commit-hash: "30acfc9d8751fdf88b9288943aaa3481fc7254a6"
+32
packages/dolmen_type/dolmen_type.0.8.1/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.8.1/dolmen-0.8.1.tbz"
+
checksum: [
+
"sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928"
+
"sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04"
+
]
+
}
+
x-commit-hash: "30acfc9d8751fdf88b9288943aaa3481fc7254a6"