Having debug levels

[jrosain]

Currently, trying to debug using the logs is a titan's task as it's cluttered with too much information.

I'd like to be able to have different debug levels, for instance:

• very high-level, e.g., allowing to follow the big steps of the proof: "Proving formula F", "Applying rule R", etc
• something in-between, e.g., what the rules are doing: "Skolemization has yielded the term t", "Instantiating to meta X", "Children have found a substitution, checking agreement"
• something low-level with locality: all the debug information of package X or Y.

(of course, what I'm saying here is only an example, I'm not asking this exact implementation).

Do you think it could be useful?