Zulip Chat Archive

Stream: lean4

Topic: Naming convention for trace classes

Michael Rothgang (Oct 08 2025 at 20:00):

As the title says: are there any naming conventions for trace class names? (Context: I added two classes in #27021, and found little documented prior conventions on this.)

Michael Rothgang (Oct 08 2025 at 20:01):

For instance: should my trace class start with Elab. or elab.? Doing set_option trace.Elab.myFooOption reads weirdly to me; set_option trace.elab.myFooOption seems more natural.

Michael Rothgang (Oct 08 2025 at 20:04):

Looking in mathlib, there current convention seems to be

  • lowercase, sometimes lowerCamelCase (e.g. adaptationNote) or snake_case options (e.g., matching tactic names, such as fun_prop)
  • sometimes prepended by a namespace, e.g. Meta.gcongr or Tactic.to_additive
  • there's no consistent pattern as to whether a tactic's trace class is in the root "namespace", the Tactic namespace or even Meta.Tactic. (The cc tactic also has Debug.Meta.Tactic.cc, in addition to e.g.Meta.Tactic.cc.merge.)

Thomas Murrills (Oct 13 2025 at 23:28):

I think the last two bullets are important problems: it would be nice to have clear, predictable conventions on what the early components of the name should be.

In particular, it might be useful to choose the conventions for namespace prefixes carefully such that we can take advantage of setting inherited := true for trace classes with that prefix.

Jovan Gerbscheid (Oct 14 2025 at 08:59):

The cc one probably came from simp, where we have trace.Meta.Tactic.simp, which I think is too long of a name.

Michael Rothgang (Oct 15 2025 at 01:40):

Cross-linking #mathlib4 > Mathlib: the Missing Manuals @ 💬

Thomas Murrills (Oct 15 2025 at 04:11):

Here's the first step of listing the available trace classes, in a manner roughly similar to what @Anne Baanen said in that thread. :)

This also sorts by name, and hijacks trace node folding to let you peek at the declaration module and docstring (if it has one). Uncomment (collapsed := false) to make all expanded by default. (Most of this code is for sorting by name, and probably already available somewhere...)

#show_trace_classes

Thomas Murrills (Oct 15 2025 at 04:37):

This code now also prefixes the list with the counts:

Found 442 trace classes.
[(Aesop, 13), (Mathlib, 56), (Lean, 365), (Batteries, 1), ([anonymous], 1), (Plausible, 6)]

Michael Rothgang (Oct 15 2025 at 10:19):

Lean trace classes, part 1

Michael Rothgang (Oct 15 2025 at 10:19):

Lean trace classes, part 2

Michael Rothgang (Oct 15 2025 at 10:20):

Lean trace classes, part 3 (everything about grind)

Michael Rothgang (Oct 15 2025 at 10:21):

All trace classes not in Lean

Last updated: Dec 20 2025 at 21:32 UTC