gilith / opentheory

The opentheory tool processes higher order logic theory packages

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.

opentheory's Issues

HOL4: different constants named "HOL4.divides.prime"

Hi,

currently HOL4's opentheory-support (--otknl) is broken. Could you please help explaining how to understand this error message:

Building directory src/boss [13 Aug, 12:40:23]
base-theorems.art                                                                                            real:    0s  user:    0s     OK
base-theorems.art                                                                                            real:    0s  user:    0s     OK
bool_defs.art                                                                                                real:    0s  user:    0s     OK
bool_defs.ot.art                                                                                             real:    0s  user:    0s     OK
/Users/binghe/ML/HOL.otknl/bin/hol.state                                                                     real:    6s  user:    8s     OK
hol4-base-unint.art                                                                                          real:   25s  user:   24sFAIL<1>
 
 FATAL ERROR: opentheory failed:
 PackageTheoryGraph.removeDead: PackageTheoryGraph.fromListSummary: different constants named "HOL4.divides.prime"
*** FATAL: Build failed in directory /Users/binghe/ML/HOL.otknl/src/boss (exited with code 1)

P. S. I'm using the latest opentheory from master branch.

Regards,

Chun Tian

Test errors at the end of building process

Hi,

It's been like this for several months. When I execute "make" from clean opentheory source directory, at the end I got some strange error outputs like this:

*** /tmp/golden-reference	2018-05-24 00:01:59.000000000 +0200
--- /tmp/test-output	2018-05-24 00:01:59.000000000 +0200
***************
*** 441,451 ****
  
  [license]
  name = MIT
! url = http://www.gilith.com/opentheory/licenses/MIT.txt
  
  [license]
  name = HOLLight
! url = http://www.gilith.com/opentheory/licenses/HOLLight.txt
  
  [cleanup]
  auto = 3600
--- 441,451 ----
  
  [license]
  name = MIT
! url = http://www.gilith.com/research/opentheory/licenses/MIT.txt
  
  [license]
  name = HOLLight
! url = http://www.gilith.com/research/opentheory/licenses/HOLLight.txt
  
  [cleanup]
  auto = 3600
make[2]: *** [mlton-diff] Error 1
make[1]: *** [mlton] Error 2
make: *** [default] Error 2

It doesn't stop me using opentheory, because the main binary is well built. But what's above error? Is it also happening on your side?

Regards,

Chun Tian

what package contains `group`?

In the repository there's plenty of packages about groups, but I can't install them via, say, opentheory install group-witness, and I didn't see them on the website. Are they not actual packages?

Modularising opentheory.sml

It is possible to load the entirety of OpenTheory's sources into Isabelle/ML.

A work in progress can be tracked in my fork: topic/isabelle.

There is one small problem, though: opentheory.sml contains a lot of code that provides a CLI entrypoint to OpenTheory. Loading it immediately quits the Isabelle process with the error message that the wrong CLI arguments are passed.

Would it be possible to provide a function val opentheory: string list -> unit instead? The entrypoint of OpenTheory could then just call that function with the CLI arguments.

Failure to build with MLton, which complains “strange constant”

Trying to build the latest OpenTheory with the latest MLton, make terminates with exit code 2 and this message:

bin/mlton/selftest
cd bin/mlton ; mlton -runtime 'ram-slop 0.4' selftest.mlb
unhandled exception: Fail: Ssa.Shrink.simplifyCases: strange constant
Makefile:180 : la recette pour la cible « bin/mlton/selftest » a échouée
make: *** [bin/mlton/selftest] Erreur 1
rm bin/mlton/selftest.sml bin/mlton/selftest.mlb

Building with polyml seems OK. I don’t know if it’s an OpenTheory issue or an MLton isssue.

install base results in parse error

$ bin/polyml/opentheory install base
auto-initialized package repo {/Users/michaeln/.opentheory}

FATAL ERROR: opentheory failed:
error in package list "/Users/michaeln/.opentheory/repos/gilith.pkg" around line 1:
<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML 2.0//EN">
<html><head>
parse error
package name install failed

Running from the root directory of the unpacked tar-file after what appears to be a successful (Poly/ML) build (opentheory help worked). On an M1 MacBook Pro (Apple Silicon), with Poly/ML --version =

Poly/ML 5.9.1 Testing (Git version v5.9-184-gbafe319b)

open term variable in sum-def?

while checking sum-def.art with my new tool (which means my code might be the one with a bug, of course), I get an error on the definition of the type operator Data.Sum.+. The theorem used to define the type operator contains a variable a:A.

With the printer which is very crude (displays constants with some type arguments, no infix operators except for =), the error message is:

Fatal error: exception in new-basic-ty-def :name Data.Sum.+
  :thm `|-
         ((\a:((HOLLight.recspace ((Data.Pair.* A B)))).
           ((Data.Bool.! (((HOLLight.recspace ((Data.Pair.* A B)))) -> bool)))
           ((\sum':(((HOLLight.recspace ((Data.Pair.* A B)))) -> bool).
             Data.Bool.==>
             (((Data.Bool.! ((HOLLight.recspace ((Data.Pair.* A B))))))
              ((\a:((HOLLight.recspace ((Data.Pair.* A B)))).
                Data.Bool.==>
                (Data.Bool.\/
                 (((Data.Bool.? A))
                  ((\a:A.
                    (a)
                    = (((\a:A.
                         ((HOLLight.CONSTR ((Data.Pair.* A B))))
                         Number.Natural.zero 
                         (((Data.Pair., A B)) (a) 
                          (((select B)) ((\x:B. Data.Bool.T)))) 
                         ((\n:Number.Natural.natural.
                           (HOLLight.BOTTOM ((Data.Pair.* A B)))))))
                       (a))))) 
                 (((Data.Bool.? B))
                  ((\a:B.
                    (a)
                    = (((\a:B.
                         ((HOLLight.CONSTR ((Data.Pair.* A B))))
                         (Number.Natural.suc Number.Natural.zero) 
                         (((Data.Pair., A B))
                          (((select A)) ((\x:A. Data.Bool.T))) (a)) 
                         ((\n:Number.Natural.natural.
                           (HOLLight.BOTTOM ((Data.Pair.* A B)))))))
                       (a)))))) 
                ((sum') (a))))) 
             ((sum') (a))))))
         (((\a:A.
            ((HOLLight.CONSTR ((Data.Pair.* A B)))) Number.Natural.zero 
            (((Data.Pair., A B)) (a) (((select B)) ((\x:B. Data.Bool.T)))) 
            ((\n:Number.Natural.natural.
              (HOLLight.BOTTOM ((Data.Pair.* A B)))))))
          a)`:
free variable (a : A) is not a type variable

Publish tagged releases

There's a tarball on the website: http://www.gilith.com/software/opentheory/download.html

Unfortunately the tarball is not stable, i.e. it is updated in-place. This is a problem because it means builds from source are not reproducible.

It would be good if

1. release tarballs contained the actual revision (e.g. 1.3.20171122)
2. a tag would be pushed to the Git repository

in article files, how to handle unknown typeOp/const?

The theory file page describes theories as \Gamma |- \Delta, so purely on the theorem level. However there are also input constants in a theory, and defined constants, if I understand correctly.

When reading an article file (the VM instructions) there seems to be no explicit operation to create a constant/typeOp by pushing it into the theory being built's inputs? Or do const/typeOp implicitly create these constants?

On a semi-related note, I've noticed that there are a few "axiom" articles (choice, infinity, etc.) but they use the axiom command which just pushes a theorem into the current theory's assumptions. So is there no real axiom in the system, only assumptions that will never be discharged?

infix notations?

I see that the tool is able to print the article's assumptions and theorems using nice sugared syntax, with binders, infix symbols, etc. Does it have special knowledge of symbols, or is there some sort of table of precedence/fixity somewhere?