Frequently Asked Questions About OpenTheory

The OpenTheory Project

The opentheory Tool

Processing Theory Packages

Package Repositories

Interfacing with HOL Theorem Provers

Exporting Theory Packages as Haskell Packages


The OpenTheory Project


Is there an OpenTheory mailing list?

There is an email list for OpenTheory users: you can subscribe and view the archives at http://www.gilith.com/mailman/listinfo/opentheory-users.


The opentheory tool


What does the opentheory tool do?

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.


Where can I download the opentheory tool?

The most recent version of the opentheory tool can be downloaded from http://www.gilith.com/software/opentheory/.


What ML implementation should I use to compile the opentheory tool?

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).


What does the opentheory tool depend on?

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.


What is the purpose of the test.sml file in the test directory?

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.


Processing Theory Packages


How can I see what theory packages I have installed?

The command

opentheory list

displays all installed packages.


How do I install the standard theory library?

The command

opentheory install base

installs the latest version of the standard theory library.


What do theory packages contain?

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.


How can I convert a theory package into a proof article file?

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.


How can I concatenate proof article files?

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


Package Repositories


Where are the packages installed?

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.


What are the NAME-VERSION.html files used for?

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.


What are the NAME.thy files used for?

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


What are the NAME-VERSION.art files used for?

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.


Why do some theory packages contain additional .art files?

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.


Interfacing with HOL Theorem Provers


How can I export a proof article file from the HOL Light theorem prover?

  1. First, install the Proof Logging in HOL Light Development Snapshot.
  2. Add the following lines to the top of a HOL Light theory file NAME.ml:

    export_begin ();;
    export_theory "THEORY";;

  3. For every theorem THM you'd like to include in the article, add an export_thm command like so:

    let THM = ...HOL Light proof of the theorem... ;;
    export_thm THM;;

  4. Add the following line to the bottom of the NAME.ml theory file:

    export_end ();;

  5. Run the NAME.ml file through HOL Light in the usual way

    ocaml
    #use "hol.ml";;
    loads "NAME.ml";;

    to generate a raw proof article file and an associated theory file:

    opentheory/export/THEORY.art
    opentheory/export/THEORY.thy

  6. The OpenTheory proof article THEORY.art can be generated with the command:

    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.


How can I export a proof article file from the HOL4 theorem prover?

  1. First, you must build HOL4 with the logging kernel. To do that, pass the argument --otknl to bin/build when you build your installation of HOL4.
  2. There are two ways to export a theory:

How can I read a proof article file into my theorem prover?

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:


Exporting Theory Packages as Haskell Packages


What is the purpose of the Haskell information in the theory files?

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.