[opentheory-users] opentheory tool to aid debugging

[Ramana Kumar]

On Fri, Oct 7, 2011 at 2:43 AM, Joe Hurd <joe at gilith.com> wrote:
> I've been thinking about this, and I was wondering whether it would be
> helpful for the opentheory tool to support debugging commands in the
> article file, along these lines:
>
> #DEBUG# stack
>
> which would print the stack at that point.
>
> What do you think? If you like the idea, what other debug commands
> would be useful?

I think it's a good idea in general to have some debugging commands,
and using the #DEBUG for them also seems good.
I don't see myself using the stack command, but it's an obvious one to include.
The ones I would find most useful are copies of all the normal
term-constructing commands (appTerm, varType, const, ref, etc.) and
commands to test whether two objects at the top of the stack are equal
(perhaps raising an exception if not), or, more specifically, whether
a theorem object is equal to a pair of a list of hypotheses and a
conclusion. I would leave it to the article writer to ensure that the
article is valid (modulo the reasons for debugging in the first place)
both with and without the #DEBUG commands being run (since I would
want them to be able to manipulate the stack and dictionary).