Mathlib/Lean/ vs Mathlib/Util/

Stream: mathlib4

[Scott Morrison]

Does anyone have a good way to formulate what belongs in the Mathlib/Lean and Mathlib/Util/ directories? I think it would be good to have this straight before we jumble things up too much. :-)

My attempt:

• Mathlib/Lean/: should contain helper functions which live in the Lean namespace, and add functionality (or merely dot-notation) to things defined in core Lean 4. In some sense this is a for_core directory, containing only definitions which are reasonable candidates for moving to the core library.
• Mathlib/Util/: user facing commands e.g. library_note, whatsnew, and #time, but also random meta programming tricks, e.g. MemoFix.lean and TermUnsafe.lean.
• Mathlib/Tactics/: tactics, with as much as possible of the "low-level" stuff that belongs in other directories factored out into those.

Corrections/suggestions welcome! I can write some READMEs to reflect any consensus achieved.

[Mario Carneiro]

I don't know if it is a useful distinction to separate term/tactic/command things in different directories. Often a single file will manifest as things in multiple categories simultaneously, and they all have a fairly similar metaprogramming interface

[Mario Carneiro]

that is, I would be inclined to put user-facing commands in Tactics as well as literal tactics

[Mario Carneiro]

Util is more for tactics that are not intended for the usual proving stuff but are either meta-programming tools like TermUnsafe and MemoFix or debugging commands like #time

[Mario Carneiro]

library_note is a bit borderline, it's primarily about mathlib organization itself which gives it a bit of "meta" feel, but we also expect it to be used throughout the library