package dolmen_type

Build not checked
  1. Overview
  2. Docs
A typechecker for automated deduction languages

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (7)

Authors

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Maintainers

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Sources

dolmen-0.9.tbz
sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a
sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74

Description

Tags

logic type typechecking first order polymorphism

Added to opam-repository:

README

Dolmen build install

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:

Acknowledgements

This work is currently in part funded by OCamlPro

Dependencies (5)

  1. uutf
  2. spelll >= "0.4"
  3. dune >= "3.0"
  4. dolmen = version
  5. ocaml >= "4.02.3"

Dev Dependencies (1)

  1. odoc with-doc

Optional Dependencies

None

Used by (4)

  1. alt-ergo-lib >= "2.5.1" & < "2.6.0"
  2. dolmen_bin = "0.9"
  3. dolmen_loop = "0.9"
  4. dolmen_lsp = "0.9"

Conflicts

None

Build status

Results of building dolmen_type with each compiler on check.ci.ocaml.org, run of against opam-repository 7cdc698. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

This version is not in the latest run; the versions below are.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
0.10 good good good good good
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure