[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.
>
>>> 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?

At first I didn't understand why you would want such a mapping, but
with my new understanding of articles and article readers, it makes
perfect sense to have a such a mapping and indeed I plan to use one
now, and definitely want the fully qualified names in the article.

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>