dolmen

A parser library
README

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

LICENSE

BSD2, see file LICENSE.

Documentation

Online documentation for the libraries can be found at http://gbury.github.io/dolmen.
There is also a tutorial.

Installation

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

Goals

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

Supported languages

Currently the following parsers are working:

  • ae (alt-ergo format) (parsing only)

  • dimacs

  • iCNF

  • smtlib

  • tptp

  • zf (zipperposition format)

The following parsers are either work in progress, or soon to be
work in progress:

  • alt-ergo format

  • coq

  • dedukti

Install
Sources
dolmen-v0.6.tbz
sha256=81b034da2de84da19fb6368aaa39135f6259ee2773ff08c8f03da9ceeb10748c
sha512=98786ff1cc5b0c8bc4cb2dfe756ae15556c3876a206546b04374826be7d0a422dd5526d93f09cb0ea0d4985b71c408c182a951d4df908399c7e04b17c91a7d70
Dependencies
odoc
with-doc
fmt
>= "0.8.7"
dune
>= "2.7"
menhir
with-test & >= "20201201"
menhir
>= "20180703"
ocaml
>= "4.08"
Reverse Dependencies