[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

Hi Rob,

I am now trying to follow this procedure and am having one or two problems.
>
> The packages natural-numeral and natural-dest seem to be exceptions to the
> rule that all the definition live in packages with names of the form
> XYZ-def.
>

That's a bug, I will fix this in the standard theory library.

The packages don't seem to come out in dependency order. E.g., the first
> few leaf packages in the natural package come out like this:
>
> natural-add-def-1.18
> natural-add-sub-def-1.3
> natural-add-sub-thm-1.3
> natural-add-thm-1.47
> natural-def-1.23
>
> But the definition of addition in natural-add-def depends on suc from
> natural-def.
>

They seem to be in alphabetical order (the default), did you give the
--dependency-order argument:

opentheory list --dependency-order '(Identity - IncludedBy) (Includes* base)

If so then there's a bug in your version of opentheory: it works on the
latest version (opentheory 1.2 (release 20131211)).

When you say "the remaining theory packages in the list can be converted to
> an article using opentheory info --article", do you mean that I can create a
> single article for them all? If so how do I do it? (opentheory info seem
> only to support a single INPUT.)
>

There are a few options here:

1. In ProofPower read in all the leaf article files one by one.

2. Create a theory file thm.thy of the form

bool-def {
  package: bool-def-1.10
}

axiom-choice {
  package: axiom-choice-1.7
}

axiom-extensionality {
  import: axiom-choice
  package: axiom-extensionality-1.8
}

bool-int {
  import: axiom-choice
  import: axiom-extensionality
  package: bool-int-1.17
}

...repeat for each leaf theory...

main {
  import: axiom-choice
  import: axiom-extensionality
  import: bool-int
  ...
}

and then run

opentheory info --article -o thm.art thm.thy

3. Here's an ugly line of perl that does the whole thing in one go:

opentheory list --dependency-order '(Identity - IncludedBy) (Includes*
base)' | grep -v -- '-def-[0-9.]\+$' | perl -ne 'BEGIN { $b = "{\n"; }
chomp; $_ =~ /^(.*)-[0-9.]+$/; print "$1 $b  package: $_\n}\n\n"; $b .= "
 import: $1\n"; END { print "main $b}\n" }' | opentheory info --article -o
thm.art theory:-

Note this relies on being able to distinguish 'definition' leaf theories by
the -def suffix, which as you point out is not the case in the current
standard theory library, but that bug will soon be fixed.

The above command takes about 45 seconds to complete on my machine and the
resulting thm.art is 6Mb in size.

Cheers,

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140320/f3b2df64/attachment.html>