Mathlib/Lean/ and locations of the meta API

Stream: mathlib4

[Thomas Murrills]

I think it might be worth reorganizing the contents of Mathlib/Lean/, or at least setting up stronger guidance on what should be where. Most of the content there extends the meta API, and so I'd also like to discuss here how we organize the meta API in mathlib in general.

I found this relevant thread from 2022: #mathlib4 > Mathlib/Lean/ vs Mathlib/Util/; Kim says of Mathlib/Lean:

Kim Morrison said:

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.

I think it might be useful to come down on one of these properties or another. Sometimes we want something in the Lean namespace, but are not seriously considering upstreaming to core. Likewise, it might make sense to organize/declare the serious upstreaming candidates somehow.

Are there any other guidelines documenting the intentions for these folders, or any other relevant discussions?

Here are a couple of issues with the current state of affairs:

• We have a couple of different ways to create locations for files, it seems:

  • we have standalone files like Mathlib.Lean.Name which start with a header of the form "Additional functions on Lean.Name"
  • we also attempt to mirror the directory structure for core to some extent, and locate our new declarations in the file it "would" be in. But this latter principle is only loosely enforced; Mathlib.Lean.Meta.Basic imports Lean.Meta.AppBuilder, whereas the dependency goes in the other direction in Lean core (Lean.Meta.AppBuilder imports Lean.Meta.Basic).
  • we have some scattered meta API in Mathlib/Util, such as Mathlib.Util.Tactic which contains only meta API declarations on modifying the local context. We also have some commands which are imported by Mathlib.Tactic.Common like whatsnew, and some which are more generally applicable, like notation3.

• It's easy for these files to get out of date, too: Mathlib.Lean.LocalContext is now only imported by Mathlib.lean itself.

• It's not always easy to access these when metaprogramming; ideally, all (theory-free) additions to the meta API could be imported all at once, at least during editing.

Mario says of Mathlib/Util/:
Mario Carneiro said:

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

Which makes sense to me, but it might be worth pinning Util down a bit more.

• Should Utils be imported in low-down files like Mathlib.Tactic.Common?
• When is something a Util, and when is it just a command in Mathlib.Tactic?
• Do we want extensions to the meta API to be in Util? If so, which go in Mathlib/Util, which in Mathlib/Lean, and which in Mathlib/Tactic?

---

Generally, I think it makes sense to ask ourselves what purpose we want to serve by whatever organization scheme we use. That is, which should we prioritize, and to what extent?

• discoverability/accessibility of utilities when metaprogramming in mathlib
• ease of upstreaming to core
• providing a (simple|broad|predictable|?) meta API
• something else?

Thoughts? :)

[Yaël Dillies]

How many files are we talking about? I was under the impression that Mathlib.Lean and Mathlib.Util both contain very few files (10-20 in total?)

[Thomas Murrills]

I'm counting 31 .lean files in Mathlib/Lean/, 30 in Mathlib/Util/. It's (ostensibly) a home for meta API, so I'd like it to be nicely organized regardless of the absolute quantity! :)

(I'm also thinking about the process of deciding where to put meta API during review/contribution; it would be nice to have this be a little more purposeful.)