Dolmen Loop is a library of useful helpers to parse and loop over statements found in automated deduction files.
A library providing flexible parsers and typecheckers for languages used in automated deduction.
BSD2, see file LICENSE.
The main method of installation is to use opam. See this page for information about how to install opam on your system. Once you have installed and configured opam, you can use the following command to install the dolmen cli and lsp binaries:
opam install dolmen_bin dolmen_lsp
Additionally, pre-built binaries for Linux and MacOs can be found on the release pages (starting from the v0.6 release, see the latest release).
The libraries can be installed using:
opam install dolmen dolmen_type dolmen_loop
The Dolmen project aims at providing an assortiment of tools to help handle languages that are used in automated deduction and formal logic.
More precisely, the Dolmen project provides:
A few OCaml libraries for:
A binary (which is using the above libraries), to parse and typecheck input files. This could be used to check a file against its language specification, and/or obtain detailed errors. See the bin doc
A LSP server so that the features of the above binary can also be used inside your favorite editor. See the dolmen lsp doc
Currently the following parsers are working:
ae (alt-ergo format)
zf (zipperposition format)
The following parsers are either work in progress, or soon to be work in progress: