Cleaning trace message option names

[leodemoura]

We do not have a consistent naming convention for trace options.
Moreover, most trace messages are mainly for helping developers to debug Lean. We need new messages/options for helping users to diagnose problems by themselves.
Work items:

• A naming convention for option names
• Design new trace for helping users to diagnose problems.
• An API for users traversing/filtering/inspecting trace objects.

[dselsam]

Recording some thoughts here while they are fresh. There are really two different hierarchies of trace messages:

1. The (dynamic) contextual hierarchy (i.e. from traceCtx calls)
2. The (static) naming hierarchy (i.e. from name-prefixes)

Accordingly, I think there are two types of trace queries that would be good to support:

• [contextual] show me everything that happens inside isDefEq calls, including in modules that isDefEq calls
• [naming] show me everything prefixed with Meta.synthInstance

Of course, they compose. One might want the Meta.synthInstance.newSubgoal calls that occur inside isDefEq calls.

Here is a rough proposal sketch starting point:

• distinguish trace classes from traceCtx classes (though the names may overlap)
• for each trace class and each traceCtx class, have a 3-way option (neutral, enable, disable)
• for a given trace { ctx = [ctx1, ..., ctxN], name = [name1, ..., nameM] }, show it if:
  • its nearest non-neutral name ancestor is enable
  • all its name ancestors are neutral and its nearest non-neutral contextual ancestor is enable

Ideally all the trace data is emitted in a single run and the data can be browsed interactively.