<div dir="ltr"><div>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.<br>

<br></div>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.<br></div><div class="gmail_extra">

<br><br><div class="gmail_quote">On Sat, Nov 23, 2013 at 4:24 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div style="word-wrap:break-word">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.<div>

<br></div><div>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?</div>

<div><br></div><div>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?</div>

<div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>