Repository files navigation

A library providing flexible parsers and typecheckers for languages used in automated deduction.

BSD2, see file LICENSE.

Online documentation for the libraries can be found athttp://gbury.github.io/dolmen.There is alsoa tutorial.

The main method of installation is to useopam.Seethis pagefor information about how to install opam on your system. Once you have installedand configured opam, you can use the following command to install the dolmencli and lsp binaries:

opam install dolmen_bin dolmen_lsp

Additionally, pre-built binaries can be found on the release pages(starting from the v0.6 release for Linux and MacOS, and starting from thev0.8.1 release for Windows). You can get them onthe latest release page.

The libraries can be installed using:

opam install dolmen dolmen_type dolmen_loop dolmen_model

The Dolmen project aims at providing an assortiment of tools to helphandle languages that are used in automated deduction and formal logic.

More precisely, the Dolmen project provides:

• A few OCaml libraries for:
  • parsing, seethe parsing doc
  • typechecking, seethe typing doc
  • writing main loops for binaries,the loop doc
• 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/orobtain detailed errors. Seethe bin doc
• A LSP server so that the features of the above binary can also be used insideyour favorite editor.Seethe dolmen lsp doc

This work is currently in part funded byOCamlPro