The opentheory tool processes higher order logic theory packages in OpenTheory format.

Cloning this repo will install a development version, which has active debugging code and includes a large collection of theories used for regressions. The latest official release of the opentheory tool without any extra development cruft lives here.

This software is released under the MIT License.

Installing the opentheory tool requires the MLton, Poly/ML or Moscow ML compiler, as well as standard system tools including GNU Make and Perl.

Clone this repo and initialize the development version:

git clone https://github.com/gilith/opentheory.git
cd opentheory
make init

By default the initialization step requires the MLton compiler, but you can change it to Poly/ML or Moscow ML by editing the top of Makefile.dev.

Use the MLton compiler to build from source and run the test suite by executing

make mlton

The opentheory tool executable can then be found at

bin/mlton/opentheory

Use the Poly/ML compiler to build from source and run the test suite by executing

make polyml

The opentheory tool executable can then be found at

bin/polyml/opentheory

Use the Moscow ML compiler to build from source and run the test suite by executing

make mosml

The opentheory tool executable can then be found at

bin/mosml/opentheory

A simple test is to display tool help, including the options available for each command:

path/to/opentheory help

A more serious test is to install the standard theory library using the command

path/to/opentheory install base

You can use

make clean

to clean out any object files.

To report a bug or request an enhancement, please file an issue at GitHub.