[opentheory-users] opentheory tool to aid debugging

[Joe Hurd]

Hi Ramana,

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?

Cheers,

Joe

On Tue, Oct 4, 2011 at 4:05 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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.)
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>