[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

I am trying to import the base package into ProofPower from the Gilith OpenTheory Repo using my prototype OpenTheory reader. I did "opentheory install base" and that seemed to work (once I had installed the md5sha1sum package from MacPorts to resolve the dependency on sha1sum). It created a directory $HOME/.opentheory with some interesting looking things in it, in particular, a subdirectory called packages with lots of subdirectories containing, inter alia, article files.

Is the idea that I should be able to read a single article file to import an entire package? Or do I need to process the theory files somehow. Or should I not be looking in $HOME/.opentheory/packages at all but doing something else?

When I look at the subdirectories of  $HOME/.opentheory/packages, some contain 1 article file and some contain 2. In bool-def-1.10 for example, there are 2: bool-def-1.10.art and bool-def.art. I can import the latter but not the former, because it attempts create a definition referring to a non-existent constant called bool-def-1.10. In base-1.132 there is just one article file base-1.132.art. When I try to import that I get the same kind of problem: it tries to define Data.Bool.T to be equal to a constant called base-1.132. What am I missing?

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131123/7c957f34/attachment.html>