[opentheory-users] parsing article information

[Ramana Kumar]

On Mon, Jan 10, 2011 at 12:38 AM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>>> opentheory info --summary is supposed to generate article summaries in
>>> a human readable form: as of now there is no machine-readable version
>>> of it other than the article file.
>>
>> Will there be? I can probably get opentheory to spit one out by
>> catching it just before it prints the human-readable version and
>> sending whatever data structures it is using to a different printer.
>
> I was planning on reusing the article format to output the summaries
> in machine-readable form at some point. I'd be interested in knowing
> what your application is for this.

My immediate application would be to check that my reader is correct.
If I can easily get the set of (term list, term) pairs representing
theorems that an article is supposed to produce from opentheory, then
I can check that after reading the article I actually did produce
those theorems.

>
>>> You are correct: the (as yet documented) show tags in a theory
>>> determines how the namespaces get transformed as names are printed. To
>>> see a pure version remove all show tags or just run opentheory info
>>> --summary directly on the article file.
>>
>> If I generate the article file with opentheory, though, the namespace
>> information is there. How do I get a pure article file for say
>> bool-1.0?
>
> When I said "pure" I meant with no namespace transformation, so all
> names print with their fully-qualified name in the OpenTheory
> namespace.
>
> What did you think of my suggestion of constructing a mapping between
> fully-qualified names in the OpenTheory namespace and HOL4 names, as I
> did for HOL Light?
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>