[opentheory-users] opentheory tool to aid debugging

Ramana Kumar ramana.kumar at gmail.com
Tue Oct 4 09:14:44 UTC 2011


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.)



More information about the opentheory-users mailing list