[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

Joe,

On 24 Mar 2014, at 05:07, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
> 
>> 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.

In the mean time I carried on processing the leaf package articles one by one. I succeeded in getting the whole thing in with out any new axioms. Initially, because the only definition of something like Set.Fold I had to hand was quite a bit different from the one in the repo, I did a devious trick whereby I included the articles that define Set.Fold and Set.size, and then used the new pragma feature to arrange to run a script just after processing those articles that did the proofs that equate the imported Set.size to the native ProofPower size function.

> 
> Over the weekend I made a new release of the standard theory library
> 
> http://opentheory.gilith.com/?pkg=base-1.158
> 
> so this command now works as intended to extract the "pure theorem" content.

Many thanks for that. I have now defined a set fold operation like the one in the repo and I can import the whole base package conservatively without any devious tricks in one go using the article file that your perl magic generates.

I have just one outstanding concern: there are no theorems in the sum package and only one in the real package (and the only operators it uses are <= and sup. There don’t seem to be any uses of real or sum in the other packages in the repo, so I haven’t really been able to test that I have got the mappings right for these packages. Any suggestions would be welcome.

I am trying with some success to load the other packages in the repo. In each case, I constructed an article for each package XYZ in the 35 package other than those included in the base package with the command:

   opentheory info —article -o XYZ.art XYZ.

The package modular seems to expect a constant called Number.Modular.modulus to be defined, but nothing defines it, so modular won’t load. The package word seems to expect a constant called “Data.Word.width” but nothing defines it. byte will load, but the word10, word12 and word16 packages won’t, apparently because they are trying to redefine a constant called Number.Modular.equivalent.

Regards,

Rob.

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