[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

On 20 Mar 2014, at 17:55, 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)).

It does work.  I have no idea how I managed to foul up the command line (I transferred it from your e-mail to a terminal window with copy-and-paste!).

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

That is the solution I am currently working with.
> 
> 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.

This looks like it will be useful when you have sorted out the glitches in the package names.

I have now imported the packages, bool, function, unit, pair, natural and option. The process is a bit clunky, but is perfectly workable. The Repo website is extremely helpful. So I would say my issues with designing a reader are resolved.

One query: is the case constant in the option package really meant to be called Data.case.none.some? That doesn’t seem to agree with the web page for the package.

Regards,

Rob.

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