[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

After sending this last email, I noticed that the bool-def theory block was
accidentally included in the thm.thy file, please ignore that theory block.

Cheers,

Joe


On Thu, Mar 20, 2014 at 10:55 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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/5f0807e1/attachment.html>