Getting Started

Requirements

You will need OCaml >= 4.00.1 or higher with ocamlbuild, zarith and the standard library.

Some modules come from ocaml-containers and are packaged with the library.

Download

You can download archives on github or use git directly :

git clone https://github.com/c-cube/logtk.git

Compilation

Additional sub-libraries can be built if their respective dependencies are met, and the appropriate ./configure --enable-foobar flag was set. For instance, to build the meta-prover library (used to detect axiomatic theories), you should run

$ ./configure --enable-meta

If menhir is installed, the parsers library Logtk_parsers can be built with

$ ./configure --enable-parsers

If you have installed qcheck, for instance via opam install qcheck, you can enable the property-based testing and random term generators with

$ ./configure --enable-qcheck --enable-tests
$ make tests

Several tools are shipped with Logtk, including a CNF converter, a type-checker, etc. They are built if the flag --enable-tools is set. API Documentation will be built provided --enable-docs is set.

After the configuration is done, to build the library, documentation and tools (given the appropriate flags are set), type in a terminal located in the root directory of the project:

$ make

Installation

If you use ocamlfind (which is strongly recommended), installation/uninstallation are just:

$ make install
$ make uninstall