[opentheory-users] parsing article information

[Joe Hurd]

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?

Cheers,

Joe