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.