package dolmen_lsp

  1. Overview
  2. Docs
A LSP server for automated deduction languages

Install

Dune Dependency

Authors

Maintainers

Sources

dolmen-0.8.1.tbz
sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928
sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04

Description

README

Dolmen

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 can be found on the release pages (starting from the v0.6 release for Linux and MacOS, and starting from the v0.8.1 release for Windows). You can get them on the latest release page).

The libraries can be installed using:

opam install dolmen dolmen_type dolmen_loop dolmen_model

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

Language Parsing Typing Model verification
ae (alt-ergo) :heavy_check_mark: :heavy_check_mark:
dimacs :heavy_check_mark: :heavy_check_mark:
iCNF :heavy_check_mark: :heavy_check_mark:
smtlib :heavy_check_mark: :heavy_check_mark: :heavy_check_mark:
tptp :heavy_check_mark: :heavy_check_mark:
zf (zipperposition) :heavy_check_mark: :heavy_check_mark:

Dependencies (10)

  1. linol-lwt >= "0.4" & < "0.5"
  2. linol >= "0.4" & < "0.5"
  3. lsp
  4. logs
  5. ocaml-syntax-shims
  6. dune >= "3.0"
  7. dolmen_loop = version
  8. dolmen_type = version
  9. dolmen = version
  10. ocaml >= "4.02.3"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None