The opentheory tool processes higher order logic theory packages
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
bin
data
doc
release
repo
scripts
src
test
.gitignore
LICENSE
Makefile
Makefile.dev
README.md

README.md

The opentheory Tool (Development Version)

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.

Install

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.

Build

Using the MLton compiler

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

Using the Poly/ML compiler

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

Using the Moscow ML compiler

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

Test

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

Troubleshoot

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.