[opentheory-users] Importing from the Gilith OpenTheory Repo

[Ramana Kumar]

I think the idea of the base package is that everything in it should
already be supported by your theorem prover, so you don't need to import it
- rather, you use it as a dependency for things you export from your
theorem prover.

That said, I think you can generate a single article that performs all the
proofs in a package, like base, using the opentheory tool with the info
command and the --article option.


On Sat, Nov 23, 2013 at 4:24 PM, Rob Arthan <rda at lemma-one.com> wrote:

> 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.
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131124/47bd1091/attachment.html>