[opentheory-users] opentheory tool to aid debugging

[Ramana Kumar]

FYI, I found an alternative method for debugging.
Namely, after logging a proof, also log the desired theorem as a pair
of a term list and a term, then immediately pop that pair off the
stack.
Then, when reading the article, if you encounter a pop command where
the top of the stack is a pair followed by a theorem, check whether
they match.
This avoids having to deal with pretty-printing/parsing in comments
and with any issues in the translation of names, since that's all
dealt with by the usual term-logging and reading machinery.

On Tue, Oct 4, 2011 at 10:14 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Is it possible to coax the opentheory tool into removing Unwanted.id
> (as it would usually do for a valid article) from an invalid article?
>
> I'm trying to debug my article writer, and I would like to use my
> reader because I can make it produce whatever custom output easily,
> but my reader doesn't deal with Unwanted.id properly.
>
> Alternatively, would it be easy to get the opentheory tool to check
> that a specific theorem (or object) is at the top of the stack when it
> sees a debugging command encoded in article comments? I've been
> thinking of pretty-printing a theorem (or logging commands to produce
> its hypothesis list and conclusion) in article comments just after the
> article commands that are supposed to prove the theorem, in order to
> find out where exactly my article writer is going wrong. (I know it's
> going wrong somewhere because eventually an inference rule command
> fails.)
>