Not any more. Between 2010 and 2017 there was a mailing list for OpenTheory users; you can view the archives at http://www.gilith.com/opentheory/mailing-list.
The opentheory tool processes OpenTheory packages, which contain statements and proofs of theorems in higher order logic. These packages are used to share proofs between the different theorem prover implementations of higher order logic, including HOL4, ProofPower and HOL Light. See the OpenTheory project home page for more details.
The most recent version of the opentheory tool can be downloaded from http://www.gilith.com/software/opentheory/.
I strongly recommend using MLton (or Poly/ML) over Moscow ML to run opentheory, for reasons of speed (MLton is about 10 times faster than Moscow ML).
Compiling the opentheory tool depends on the GNU Make and Perl system tools, in addition to an ML implementation.
Running the opentheory tool depends on the curl and shasum system tools.
This file is part of the self-test for opentheory. The file is run by Moscow ML, MLton and Poly/ML, generating the files mosml-result, mlton-result and polyml-result (respectively). These are compared to the expected result in the result.ok file.
The command
opentheory list
displays all installed packages.
The command
opentheory install base
installs the latest version of the standard theory library.
Theory packages contain statements and proofs of theorems in higher order logic. The command
opentheory info --theory NAME-VERSION
outputs a summary of the theory contained in the package NAME-VERSION in text format, and the command
opentheory info --document -o THEORY.html NAME-VERSION
outputs a summary of the theory in HTML format to the file THEORY.html.
The command
opentheory info --article -o THEORY.art NAME-VERSION
outputs the theory contained in the package NAME-VERSION in proof article format to the file THEORY.art.
To concatenate a series of proof articles files input1.art, input2.art, input3.art, ... into a single article file output.art create a theory file tmp.thy of the form
art1 {
article: "input1.art"
}art2 {
import: art1
article: "input2.art"
}art3 {
import: art1
import: art2
article: "input3.art"
}...repeat for each input article file...
main {
import: art1
import: art2
import: art3
...
}
and then run
opentheory info --article -o output.art thm.thy
By default, the opentheory tool installs packages to a repository in the directory ~/.opentheory. It is possible to specify a different package repository directory using the global option -d, --root-dir DIR.
The files for package NAME-VERSION are stored in the subdirectory packages/NAME-VERSION of the package repository.
When the theory NAME-VERSION is installed into the packages/NAME-VERSION subdirectory of the package repository, a package document file NAME-VERSION.html is automatically generated that contains a summary of the theory in HTML format.
The theory source file NAME.thy, normally found inside the packages/NAME-VERSION subdirectory of the package repository, contains instructions for how to construct the theory contained in the package. This might be as simple as
main {
article: "NAME.art"
}
which says that the theory is constructed by reading the article file NAME.art, but more complex theory source files are possible that import and combine other theory packages.
Theory files also contain some meta-information about the package in the form of tags, for example:
name: bool
version: 1.0
description: Boolean theory
author: Joe Leslie-Hurd <joe@gilith.com>
license: MIT
When the theory NAME-VERSION is installed into the packages/NAME-VERSION subdirectory of the package repository, a package theorems file NAME-VERSION.art is automatically generated that contains the statement (but not proof) of every theorem contained in the the theory package.
This file is used to optimize theory dependency computations performed by the opentheory tool. Most uses of the theory package will require both the statements and proofs, which the opentheory tool can output in article file format.
The article: directive in a theory source file causes the opentheory tool to read in a file in proof article format—such files have extension .art.
export_begin ();;
export_theory "THEORY";;
let THM = ...HOL Light proof of the theorem... ;;
export_thm THM;;
export_end ();;
to generate a raw proof article file and an associated theory file:ocaml
#use "hol.ml";;
loads "NAME.ml";;
opentheory/export/THEORY.art
opentheory/export/THEORY.thy
opentheory info --article -o THEORY.art opentheory/export/THEORY.thy
Note: A simple way to rename the HOL Light type operators and constants you define in NAME.ml as part of the export is to add extra lines to the opentheory/base/base.int file.
Read the proof article file NAME.art into your theorem prover, using existing type operators, constants and theorems for the ones in the external type operators, external constants and assumptions sections of the article summary.
If your higher order logic theorem prover does not already have a reader for proof articles, you have the opportunity to contribute to the OpenTheory project by implementing one yourself! To do this you need to write an ML function that takes as input the article file name, and reads in the commands in the article file one by one, processing them exactly as described in the article file format standard.
It might be useful to refer to the article reader implementation in the opentheory tool (although opentheory needs to keep track of more state to rename and compress articles), in particular the following files in the release:
This means that there are definitions in the theory package that can be exported as a Haskell package. For example, the definitions in the base theory package are exported to the opentheory Haskell package on Hackage.
In general, the Haskell package name is simply the theory name with opentheory- prepended, unless there is an explicit haskell-name declaration in the theory file that overrides this.
You can find some (mostly outdated) information on a previous version of this Haskell export functionality in the Maintaining Verified Software paper and talk in the Publications section of the OpenTheory project home page.