[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

Sorry I'm late to the thread - I have just jumped 8 time zones to visit the
UK for a while.

As Ramana said, the opentheory tool is supposed to be the main way that you
interact with the theory directory in ~/.opentheory, and Ramana gave you
the right invocation to covert a theory package to an article file:

http://www.gilith.com/research/opentheory/faq.html#convert-theory-to-article

The NAME-VERSION.art article file you found inside

~/.opentheory/packages/NAME-VERSION

is actually a cache of the theorems in the theory package stored in article
format, where the "proof" of each theorem just uses the axiom command.
These theorem caches are used to match dependencies between packages
without needing to read in the whole proof in the theory package.

Cheers,

Joe



On Sun, Nov 24, 2013 at 3:29 PM, Ramana Kumar <ramana at member.fsf.org> wrote:

> You can also use the -o or --output option instead of shell redirection.
>
>
> On Sun, Nov 24, 2013 at 2:46 PM, Rob Arthan <rda at lemma-one.com> wrote:
>
>> Ramana,
>>
>> On 24 Nov 2013, at 09:45, Ramana Kumar wrote:
>>
>> 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.
>>
>> I want to import it so I can have a better look at it. The kind of thing
>> I want to do is to make sure that my reader can prove all the assumptions
>> in it and to make sure that my writer only uses definitions and theorems
>> that it provides when it is writing out a ProofPower inference as a
>> sequence of OpenTheory inferences.
>>
>> 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.
>>
>> I invoked opentheory like this:
>>
>> opentheory info --article base
>>
>> and after 12 minutes learnt that I should have invoked it like this:
>>
>> opentheory info --article base >base.art
>>
>> I am then able to import all 1117 theorems and 3 assumptions from
>> base.art into ProofPower.
>>
>> Thanks!
>>
>> Rob.
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>>
>
> _______________________________________________
> 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/20131125/62dcb12d/attachment.html>