package dolmen_type

  1. Overview
  2. Docs
A typechecker for automated deduction languages

Install

Dune Dependency

Authors

Maintainers

Sources

dolmen-v0.5.tbz
sha256=b9a6f80bf13fdf1fd69ff2013f583582fa00e13c86ee6f800737fabcfd530458
sha512=84b8c18e56b3fb20674af0a3729b7e15e543f21b0062c565b575b994388eb55ee8123e5d3d31f5f1042b204544b3084089a024c742ab741ddd7e18b5641dd399

README.md.html

Dolmen

A library providing flexible parsers for input languages.

LICENSE

BSD2, see file LICENSE.

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 feature sof the above binary can also be used inside your favorite editor. See the dolmen lsp doc

Documentation

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

Supported languages

Currently the following parsers are working:

  • dimacs

  • iCNF

  • smtlib

  • tptp

  • zf (zipperposition format)

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

  • coq

  • dedukti

Build & Install

You need opam to install the developpement version of dolmen. You can installations instructions for opam here.

To install all packages provided by dolmen:

opam pin add https://github.com/Gbury/dolmen.git

Manually, you'll need to first install the dependencies needed by dolmen, the easiest way is to pin your local copy of dolmen like this:

# At the root of your local dolmen repository
opam pin add --no-action ./
opam install --deps-only dolmen dolmen_type dolmen_loop dolmen_bin dolmen_lsp

Once the dependencies have been installed, you can build the project with:

make
OCaml

Innovation. Community. Security.