[opentheory-users] parsing article information

[Ramana Kumar]

opentheory info --summary pkg gives me some useful information, in
particular the list of theorems the package ought to produce.
I want to use this to test my HOL4 article reader, so I can compare
the theorems I generate against what the article is supposed to
generate.
(info --summary could be helpful in automatically determining required
thms/types/constants too)

Q1: Is this information available by a more appropriate means than
calling info --summary?

Q2: The article file for bool-def-1.0, say, seems to talk about
constants with the prefix "Data.Bool.", but in info --summary this
prefix is stripped off. How should I find out that there may be a
prefix like this to deal with? (I saw some "show" thing in the output
from opentheory once - is that documented? what does it mean?)
Q2.1: How should I deal with the prefix? Should the article reader
strip it off names in the article file, so that the generated theorems
end up looking more like info --summary, or should I create theorems
with the prefix and add the prefix when parsing the summary?

Q3: Are there any published rules or grammar for how info --summary
terms (and theorems) are printed?

Q4: info --summary doesn't give the arity of the required type
operators or the types of the required constants... I think these can
be figured out by actually reading the article, but by then it might
be too late for someone making a call to read_article who wants to
provide the requirements. can+should opentheory print this information
(maybe optionally)?